Debate on Lean's Dominance in Proof Assistants and Alternatives like Metamath

Lean's Growing Prominence

Over the past three years, the Lean proof assistant has solidified its position within the mathematical community. This momentum was significantly boosted by projects like Kevin Buzzard's Xena Project and Peter Scholze's Liquid Tensor Experiment, alongside the conversion of Mathlib from version 3 to version 4 and the launch of the Lean FRO.

Questioning Lean's Inevitability

Despite Lean's current widespread adoption, the article raises the question of whether organizations should seriously support alternatives. The author suggests that Lean's popularity might stem more from the influence of prominent individuals who adopted it rather than its objective superiority as an interactive theorem prover (ITP).

Metamath as a Potential Alternative

Metamath is presented as a strong candidate for an alternative ITP. One key advantage is its higher assurance of correctness, particularly relevant for validating AI-generated proofs, given that Lean has experienced soundness bugs. This is attributed to Mario Carneiro's work on Metamath Zero.

Additionally, Metamath's foundation in set theory addresses concerns some mathematicians have with the propositions-as-types philosophy used by Lean and other leading ITPs like Rocq and Agda. Other set-theoretic ITPs mentioned include Mizar and Isabelle/ZF.

Impact of AI on ITP Development

The most significant argument in favor of Lean has been its extensive library, Mathlib, which was previously considered infeasible to replicate for other ITPs. However, the article suggests that recent advancements in AI models for writing formal mathematics make it plausible to build analogous libraries for alternative ITPs, potentially leveling the playing field.