alt Hacker NewsScore one more for CAM (computer assisted math) and automated proving tools.
In a world where your academic colleagues will only pay attention to your paper if it comes with a Lean or Coq proof (or at least an MM sketch), we would not be in a "it will take years just to understand the paper" type situation.
The title of the paper would then be: "Birational Invariants from Hodge Structures and Quantum Multiplication: the source code".
Other major offender in that space is Mochizuki's [1] "Inter-universal Teichmüller theory".
The very name of the work uses words that make no sense in common English.
Replies
_zoltan_ • last Saturday at 4:13 AM
what progress has been made on understanding Teichmüller theory in the past decade? not a lot...
Nah, machine verification just tells you that a theorem is true. It does nothing to help you understand it. An Lean formalization of Wiles' proof of FLT would be as incomprehensible to me as Wiles' non-formalized journal article is.