That being said, constructive math is still a great idea.
Edit: it's clear that the original four-color proof had nothing to do with this kind of formalization, it was just the debate that got me thinking about it. And tools like Lean4 aren't limited to constructive math afaik.
In fact, Lean is strongly geared towards classical logic: most of its tactics assume and use classical logic, especially the excluded middle.
As an ardent proponent of formalizing proofs, I still have to disagree with this framing. Mortal mathematicians don't need any excuse not to formalize their stuff. They rather need a reason to do it. One can give lots of reasons but mathematicians often don't know them or don't agree with them.
An important point is, for example, to understand that most formalizing effort is not primarily motivated by a desire to make sure there are no errors in the math.
Is this because the proof author is generally confident that the proof is essentially correct?
https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli...
tl;dr: contradictory stuff even gets published in the likes of Annals of Mathematics, and even top journals are reluctant to retract published proofs that have later been shown to be false (which in itself shouldn't be possible).
Like it or not, the reasons for formalizing mathematics abound, and they have a lot to do with the fact that humans are fallible, but mathematics shouldn't be. The incredibly tedious work of tracking down a proof's correctness to the last axiom is, while overwhelming for humans, exactly the kind of work that classical computers excel at.
If some result is wrong (as opposed to just details in a proof which could be fixed) and it turns out to be an important result, the mistake is found eventually. This fairly rare occurrence wastes some time for people who maybe used the result and build upon it, but arguably a lot less time than it would take to formalize all papers with existing tools. This might change in the coming decades as formalization becomes easier.
The perspective that this is not the main motivation is also the position of people working on Lean's Mathlib. E.g. Kevin Buzzard has said this at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4...
> If my work in pure mathematics is neither useful nor 100 percent guaranteed to be correct, it is surely a waste of time. So I have decided to stop attempting to generate new mathematics, and concentrate instead on carefully checking "known" mathematics on a computer
I also remember him saying sth along the lines that his concern about how much of recent math is reliable being a major inspiration for his initial involvement in an interview (could have been for Quanta Magazine or so), but couldn't find it now, so can't verify.
Aside from that, the statement you're quoting is deeply puzzling to me. No work is ever "100% guaranteed to be correct", not even something formally verified by a computer, so that statement is either false, vacuous concerning correctness or he didn't mean it literally... (Maybe 100% really means 99.99999% of the time, or something)
Jokes aside, I'm pretty sure he was aware of the limitations at all times, and I'm reading this statement in the context of his examples in the presentation. There's a nice story in a Quanta interview about how he was approached by Peter Scholze to help formalize part of a proof. Scholze had asked whether they'd gone through his recent work, and when he said Yes, Scholze asked whether they'd carefully checked theorem 9.1. Buzzard said no, they didn't have enough time left when they got to chapter 9. And Scholze said, see, that's the problem, is anyone in the world really going to check 9.1? And then there are the stories in the presentation, where entire published proofs are put in question, not because of any direct mistake by the authors, but because of a problem in a lemma they used from previous work. This kind of transitive dependency chain could go down multiple papers, and there's really no guarantee that the later results are salvageable. So it seems to me that formalization would be a great practical tool to mitigate those problems.
And then yes, it's also super cool in its own right (imho), just the fact of collecting the knowledge, and then the related work might also prove useful for formal verification (of hard/software systems), which has practical relevance, and mathlib might also just happen to become a great enabler for developing math-focused AI. So lots of good reasons to do it, but correctness might still be the most direct payoff: Terry Tao has a different blog post about how he found a (fixable) error in a recent proof of his, thanks to Lean. If that happens to him on one of the first occasions where he uses the tool seriously, then we can only guess what's waiting to be fixed (or thrown out) in the whole body of published mathematics.
> formalization would be a great practical tool to mitigate those problems
Yes, I agree. V. Voevodsky's story is a great example how things can go wrong and I very much admire him for the consequences he took from that.
However, if some mathematician has the goal of advancing a certain field, I don't think you can argue convincingly in 2023 that they should formalize their papers because making extra sure there's no errors is worth the time investment in terms of advancing the field. Again, I expect to see this slowly change.
It was always clear to me that formalization was the future of math ever since I heard about the four-color theorem. What I did not anticipate, and what Terry seems to take in stride here, was that we'd get an AI that can almost do the job of writing the math as well around the same time as formalization starts to gain traction. The fact that I get to learn about it from the most friendly and humble generational genius is just the cherry on top.