alt Hacker NewsThe response by some in the field of mathematics to this repo is ... I guess not unexpected; but it's quite disappointing.
I sympathize with those who've worked on some problem for years and now don't have something to work on; it's been a part of their identity. I also especially sympathize with those whose career tracks and plans were thrown in disarray.
That being said, I absolutely cannot understand how one can't be excited and happy and enthused about these advances in one's field. Assuming just that the ones with formal lean proofs are actually true, these are reportedly huge advances. Even if folks don't understand it YET.
It is because in fact MOST mathematicians (and researchers) don't really just want "advances" in their field. They also want to have some significance and play a role in it. What's the point of doing research, which takes a lot of work for much less pay than industry, except to have some of the glory?
I didn't go into math so I could read the results of others all day. I went into it to contribute meaningfully, and I certainly don't consider interpreting the results of a machine to be a meaningful contribution.
Your perspective is just the perspective of a consumer of things. In that case, it doesn't matter where they come from.