Re:Classification of Finite Simple Groups Formalized in Lean
by semolinapudding on Wednesday October 28, 2026 @08:19AM
(#50272422)
Im' not sure he'd say that -- Per Martin-Löf's original work was to develop a computational and predicative foundation for constructive mathematics à la Bishop.
Lean's type theory kinda gives up on that idea: Mathlib gleefully postulates impredicative propositions with the axiom of choice, quotient types, etc. All in all, I'd say that Lean is much closer in spirit to De Bruijn's AUTOMATH project (which pre-dates Martin-Löf!), whose goal was to formalise classical math textbooks using dependent types.
Re:Classification of Finite Simple Groups Formalized in Lean
by Ericson2314 on Wednesday October 28, 2026 @02:08PM
(#50278268)
I am saying that Martin-Löf would see his work in Lean, not mathlib. Mathlib is a library. In Lean you can "contain" classic reasoning to certain parts of the code base, and that is also true in the original MLTT: you can postulate classical axioms as functions in scope.
Re:Classification of Finite Simple Groups Formalized in Lean
by semolinapudding on Thursday October 29, 2026 @06:55AM
(#50287083)
Even without Mathlib, Lean's type theory is impredicative. Martin-Löf does not consider impredicativity to be constructive.
What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).
I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.