New math book rescues landmark topology proof

Because programmatically checked proofs don't work the way you think they do.

And even programatically checked proofs are still programs. And programs still need code review.

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.

> Why don't serious math journals require programmatically checked proofs for all publications

Because mathematics has more or less worked fine for decades without it, and most mathematicians aren't programmers and aren't interested in it. Proofs are for understanding, not for technical correctness (though obviously the latter is very important). A good proof convinces someone that it's true; convincing a computer that it's true is probably tangentially useful, but not very interesting to most mathematicians. They mostly want to be expanding the frontiers of mathematical knowledge, not painstakingly encoding proofs that they already believe (and, crucially, that their peers also already believe) into a computer system.

That's not to say proof checkers aren't interesting in their own right, but there's lots of really quite good reasons why mathematics goes without them almost all of the time. Formal methods bring a lot to computing, where our programs fall apart constantly, but mathematical proofs almost always don't fall apart. And in computing, almost all programs don't have formal proofs of correctness! If any area needs them, it's in computing, not mathematics. You might as well ask why every compiler doesn't come with a proof of correctness: because it's already hard enough to build a compiler, let alone the monstrosity that would be a formal proof.

The added benefit to a computer-checked proof is usually small to nil, and it's a ton of work. Like, way more work than just writing the proof.

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.

Would it though? Are proof checkers much more complicated than LaTeX?

If mathematicians are in certain ways similar to developers, I'd expect them to hate fighting with the layout of their papers, and love fighting with a proof checker for the formulas.