Comment by disconcision
2 years ago
this may be changing. as we speak. terence tao has recently been working to formalize existing work in lean. and has already found a bug in one of his published proofs. i think there will always ish be a need for mathematical proofs in the contemporary sense, but at this point i don't think its too implausible to suggest a future where the mathematical mainstream moves towards some hybrid mathematical exposition of computationally verified artefact.
I think it's likely that axiomatic approaches, and formal approaches will continue to produce interesting results and have some effect on regular mathematics.
But this is very different to suggesting that most regular mathematics will switch to using formal proofs. There's a big ergonomics gap at the moment.
An analogy could be to look how pure mathematicians look down on applied mathematicians' work, the applied mathematicians don't care, they just get on with their own standards. You need regular mathematicians to choose to switch over en masse, what will compel them to do that?
…success by Tao and Scholze in formalizing their work and gaining appreciable benefits such as correcting technical errors.
Which is happening right now — and the younger mathematicians who are supporting those efforts (and more broadly, things like Lean libraries) are gaining the experience while making the ergonomic changes.
That is, the person you’re replying to isn’t unaware of the historic problems: they’re pointing out that migration is starting now with early adopters like Tao and Scholze.
I think a little hesitance on the overall success of these sorts of projects is prudent, given the history of axiomatic and formal expections and reality.
But let's say they make huge amounts of progress - they might improve the ergonomics enough that the formal foundations of mathematics will be brought into mathematics departments as a standard, legitimate and popular subject. But I still can't see how this would affect most mathematics.
1 reply →