Is the Mathematical Community Stuck with Lean or Can Alternatives Rise?
Are We Stuck with Lean?
I question whether the mathematical community is permanently locked into Lean as the dominant proof assistant. While Lean benefits from significant momentum and the Mathlib library, I argue that alternatives like Metamath offer superior soundness assurance through Metamath Zero and a set-theoretic foundation. With advancing AI capabilities, building competitive libraries for other systems is now feasible, suggesting we should not dismiss viable alternatives that could better serve our needs.
I am, however, suggesting that having a viable alternative ITP that has higher assurance of soundness and that is based on set theory would be a good thing for the mathematical community as a whole.