Is there a machine-verifiable version ?
I mean ... 800 pages, I'd say the benefit of the doubt applies.
replies(1):
And (my hot take:) the formal correctness is important, but not really that important in math. Sure, we hope the proofs are correct, but the idea why the proofs are correct is often more important. Humans are not a formal verification machines, and we're often interested in why something is true (and when exactly, i.e. how does it generalise), instead of just asking a binary question. So taking this into account, even if there are holes in the current argument, the important thing is that the experts believe they can be fixed, and the insight we gained along the way.
Edit: I want to back my hot take a little:
* The four color theorem is famous for being the first major theorem to be proven using a computer (using exaustive search on a large search space - too large for human to verify). This was very controversial for the time (maybe still is), because we gained no insight into the problem! Exhaustive search doesn't begin to explain why this is - or is not - the case.
* Even more perversely, It's possible that ABC conjecture was proven in 2012 by Mochizuki. But the proof is very hard to read (very briefly: basically nobody understands it, and Mochizuki was - supposedly - very non-cooperative and refused to answer questions. Some experts claimed holes but their concerns were - quite rudely - dismissed as misunderstanding). Now we live in a split world, where most of the world consider the conjecture unproven (because we can't understand it and learn from it), but some universities consider it proven (because Mochizuki is an expert, and nobody was able to find a mistake and convince the world they're right). In other words, it's a mess.
In both cases, the problem was that we care about understanding the problem, not about just asserting something is true or false.
* https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ discusses a few recent usages in recent papers and the author's grant to formalize Fermat's last theorem.
* The liquid tensor experiment (https://www.quantamagazine.org/lean-computer-program-confirm...)
* Feit-Thompson was formalized in 2012.
I do largely agree that formal correctness within mathematics is not as important as it may seem, though this doesn't mean formal verification of a proof is completely orthogonal to understanding it - you can't formally verify something without really understanding the proof in the first place.