Are We Stuck with Lean?
5 hours ago
- Three years ago, the author gave a talk suggesting that the mathematical community had a narrow window to choose a proof assistant, with Lean gaining momentum but not yet inevitable.
- The central question is whether any organization would seriously support an alternative to Lean, such as Metamath.
- Metamath offers two advantages: higher soundness assurance due to Metamath Zero, and a set-theoretic foundation that addresses concerns about the propositions-as-types philosophy.
- Lean's popularity may be driven by prominent figures rather than objective superiority; its main strength is the Mathlib library.
- AI's progress in formal mathematics makes it feasible to consider building analogous libraries for other provers, though quality remains a challenge.
- The author advocates for a viable alternative to Lean for the community's benefit, but this requires institutional support whose source is unclear.