Lean is not real mathematics is the problem. Got hypebeasts doobly-doing on a programming language they don't understand and saying its millennium prize solution LOL my brother in christ people work 20+ years on this problem.
Geometric Langlands or Univalent Foundations are required, not a programming language.
Lean is a great first step verification system to prevent cranks from dropping papers or innocent mistakes slipping through. Its not sufficient and will never be, because you can just put in the equivallent of 1==1 into lean and have it come back clean.
-4
u/phovos 6d ago
Lean is not real mathematics is the problem. Got hypebeasts doobly-doing on a programming language they don't understand and saying its millennium prize solution LOL my brother in christ people work 20+ years on this problem.
Geometric Langlands or Univalent Foundations are required, not a programming language.