Total amateur here, but it strikes me that one important difference is that performance matters in software in a way that it doesn’t in mathematics—that is, all proofs are equally valid modulo elegance. That means that abstractions in software are leaky in a way that abstractions in mathematics aren’t.
In other words, in software, the same systems get reused in large part because they’ve been heavily refined, in terms of performance, unexpected corner-case behavior and performance pitfalls, documentation of the above, and general familiarity to and acceptance by the community. In math, if you lay new foundations, build some new abstraction, and prove that it’s at least as powerful to the old one, I’d think that you’d be “done” with replacing it. (Maybe downstream proofs would need some new import statements?)
Is this not the case? Where are people getting stuck that they shouldn’t be?
The value of a proof is not only its conclusion but also the insight that it provides through its method.
The goal of mathematics is not to prove as many theorems as possible but rather to gain an ever deeper understanding of why certain statements are true. The way that something is proved can be more or less useful to advancing that goal.
As an example the elementary proof(s) of the prime number theorem are just about as famous as the original proof. Sometimes the second bite of the cherry is even juicier than the first.
Tbh, elegance is something programmers should strive for too. Elegant code is easier to build upon, easier to read/understand, easier to modify, easier to adapt. For all the same reasons mathematicians want elegance. Though it's true for many domains. People love to throw around the term "first principles" but that's not something you (usually) start at, that's something you derive. And it's usually not very easy to figure out
Ultimately, a proof is an argument that something is true. The simpler "more elegant" proof is generally going to be more convincing.
You're assuming that the point of interactive theorem provers is to discover new mathematics. While that's an interesting research area, it seems like the more practical application is verifying proofs one has already discovered through other means.
How good do you think AI will be at proving new results given that training set?
Math is going to change, and change massively. There's a lot of whistling past the graveyard going on from those who are frightened by this prospect.
What LLMs are good at is organizing concepts, filling in detail, and remembering to check corner cases. So their use should help mathematicians to get a better handle on what's terra firma and what's still exploration. Which is great. Proof by it-convinced-other-mathematicians doesn't have a flawless track record. Sometimes major theorems turn out to be wrong or wrong-as-stated. Sometimes they're right, but there's never been a complete or completely correct proof in the literature. The latter case is actually quite common, and formal proof is just what's needed.
Refactoring formalized developments is vastly easier than refactoring software or informal math, since you get verified feedback as to whether the refactoring is correct.
But that is because everyone has to switch to the new system. There are no shortage of experimental OSs that do things in different ways. They fail because of switching costs not because making them is hard.
A machine checked proof is valid if it happens once. You dont need the whole world to switch.
Terence Tao is actively using LEAN and working with the LEAN community to prove leading edge mathematics.
That's fine in math. Math is true or it is not. People who overturn popular conjectures in math get fame, not approbation.
Being able to prove things in something like Lean means that stuff like Mochizuki's work on the abc conjecture could be verified or disproven in spite of its impenetrability. Or, at the very least, it could be tackled piecemeal by legions of students tackling a couple of pages every semester.