Score 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.

[1] https://en.wikipedia.org/wiki/Shinichi_Mochizuki

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.

what progress has been made on understanding Teichmüller theory in the past decade? not a lot...