The consensus is that proof is in fact incorrect. People tried really hard (like putting in a year of effort) and most converged to the same place, that proof of 3.12 is incorrect or has a gap. Peter Scholze (who won Fields Medal) and Jakob Stix did a writeup. People seem to think Shinichi Mochizuki correctly reduced ABC conjecture to 3.12, but didn't prove 3.12, and also are doubtful about the whole program because 3.12 doesn't seem any easier than ABC conjecture while complicating everything.
replyhttps://ncatlab.org/nlab/files/why_abc_is_still_a_conjecture...
Not quite?
It is more that
1) someone has gone through it, identified a step he thinks isn’t a valid step, and the author hasn’t been willing to work with that person
2) most consider the proof, due to its length combined with those doubts as to its validity, not worth their time and effort to work through and understand (because it would take a lot of time, and they have jobs to do, doing research and teaching, etc.)
replySome of the best mathematicians in the world tried to study his work, found flaws he did not address, and somehow there’s someone every week suggesting there’s a conspiracy against this guy. It’s really baffling. AI will probably help him move on by lean verifying his proof is wrong…
replyBy this point, he is very much nutso enough that a Lean certified counterexample to his theories would not dissuade him. His response would be either that the formalization is incorrect (with no coherent insights on how to fix it), or worse, Lean itself is a tool of Western imperialism and incapable of properly explicating his ideas. He has, in the past, ranted against such things as monotheism and English grammar as being the reason for his theories' lack of popularity.
replyIIRC he has expressed support in the past for attempts to formalize IUT in Lean, but we'll see where that really goes, because he's absolutely not clearheaded enough to lead such a project himself.
Project LANA ran into the same roadblock as Scholze and Stix, when they attempted to formalize the proof in Lean.
reply[dead]
reply