I'd be interested in whether proofs like these will be formalized in proof assistants that can be checked with computer code, so that it removes doubt of error. It's something in math I'd like to see become more prevalent.
Something at this level is still far away, but it should be possible in theory. Last time I checked, there was still a lot of work to be done with formalizing geometric objects in Lean (the only proof assistant I have experience with). We are more in the stage of formalizing proofs from undergraduate books, whereas the proof of the 4-dimensional Poincare conjecture is multiple orders of magnitude more difficult.
From my understanding and limited experience, formalizing complex objects is quite difficult. A long proof where the objects are integers or algebraic relations might be easier than even defining a manifold. For example, with Lean, it was a lot of work to even define a perfectoid space -- which, to be fair, is a complicated object -- much less, say anything interesting about it.
If someone has more experience with other proof assistants, I'd be interested to hear about how far away a proof like Freedman's would be. My understanding is that each one (coq, agda, lean, etc) has certain drawbacks or benefits and can describe some concepts more easily than others, but "high-level" proofs are few and far between for all. For example, Coq has a verification of Feit-Thompson Theorem which is really cool, but I don't think there are many complex objects in there. As far as I know, it's groups, linear algebra, generator and relation computations -- all of which are pretty well handled by computers. On the other hand, to even begin a verification of Fermat's Last Theorem, you would have to first build up the entire scaffolding of modern (well, second half of the 20th century at least) algebraic number theory, quite a feat in itself.
The problem is, once you have a proof that everyone agrees is correct, what's the incentive to painstakingly translate it into something a computer also agrees is correct?
Yes, you might turn up some "bugs" in the proof, but proof bugs can almost always be ironed out. It's a very rare proof that is accepted and then falls apart later. If proofs were as "buggy" as computer programs- falling apart all the time- then there'd be a much bigger appetite for proof checkers. But as it is, mathematical peer review seems to work awfully well.
I agree that it's rare that a proof is accepted and falls apart later, but it does happen occasionally.
Somewhat famously, Voevodsky turned his attention to mathematical foundations, including proof assistants, at least in part because he was spooked that a part in one of his big papers was later shown to be incorrect. (Interestingly, someone much less known pointed this out in a preprint but it was, from my memory, largely ignored for some time -- who's going to believe a nobody versus a Fields Medalist?) There's a talk that Voevodsky gives at (I think) IAS, where he mentions this.
The whole talk is interesting, but slides 8-13 talk about the topic at hand. In particular:
> This story got me scared. Starting from 1993 multiple groups of mathematicians studied the “Cohomological Theory” paper at seminars and used it in their work and none of them noticed the mistake.
> And it clearly was not an accident. A technical argument by a trusted author, which is hard to check and looks similar to arguments known to be correct, is hardly ever checked in detail.
...
> It soon became clear that the only real long-term solution to the problems that I encountered is to start using computers in the verification of mathematical reasoning.
There's plenty of incentive to do that actually, since a translation of a proof that had not been formalized before yields a much clearer proof than anything a human could write on her own. This is doubly true when some "bugs" are found and "ironed out" in the process - even seemingly trivial bugs can trip up the reader and obscure interesting sr
structure. In fact, a truly novel formalization is pretty much publishable work in and of itself. The problem is not incentives; it's more of a lack of willingness to work in an area that's very fragmented still and makes it way too hard to reuse existing results.
It's possible, but difficult. Proofs written by humans tend to not include a bunch of relevant details and assumptions. They consist of lines like "We have some property/object/logical statement X, then by theorem Y we have Z", but often don't state how exactly they are using theorem Y to get result Z. There's often some additional algebraic or logical manipulation, or some simplification of terms, or implicitly using some other theorem or lemma that seems obvious to the writer.
Getting a computer to automatically find proofs of statements is difficult (impossible in general), and I wouldn't be surprised if converting a standard human-written proof into a formal proof system is just as hard.
> I'd be interested in whether proofs like these will be formalized in proof assistants that can be checked with computer code, so that it removes doubt of error.
