GoKawiil$\begingroup$
Three years ago, I gave an informal talk to my colleagues, suggesting that we were living in the Dumey microsecond when it would still be possible for the mathematical community to throw its weight behind the proof assistant of its choice. Lean already had a lot of momentum because of Kevin Buzzard's Xena Project and Peter Scholze's Liquid Tensor Experiment, but at the time I gave my talk, Terry Tao had not yet taught himself Lean, and the conversion of Mathlib from version 3 to version 4 had just barely been completed. Similarly, the Lean FRO has just barely been launched. Lean did not yet seem as inevitable as it seems today.
My question is:
Are there any prospects for any organization to seriously support an alternative to Lean?
To make the question more concrete, let me suggest Metamath as a candidate. (To be clear, I personally have no vested interest in Metamath or any other specific theorem prover.) I see two things going for Metamath.
One of the primary reasons the mathematical community is interested in interactive theorem provers (ITPs) is that they provide a way to validate whether AI-generated proofs (or complicated human proofs, for that matter) are formally correct. As recent events have demonstrated, Lean is not immune to soundness bugs, and finding obscure soundness bugs is the forte of AI. Because of Mario Carneiro's work on Metamath Zero, the assurance of correctness would be significantly higher if we were to use Metamath. Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean and other leading candidates (e.g., Rocq, Agda), as eloquently articulated by James Hanson's recent MO post.
Again, I'm not wedded to Metamath; Mizar and Isabelle/ZF are also leading candidates for a set-theoretic ITP (though they do not enjoy a counterpart of Metamath Zero). I am concerned, however, that much of the popularity of Lean can be traced to the fact that a few prominent people happen to have picked it and given it a high profile, not necessarily because it's objectively the best ITP for the job that we want done.
The biggest argument in favor of Lean, in my mind, is Mathlib. Replicating Mathlib for any other ITP would, until recently, have seemed completely infeasible in practice. However, given how good AI models have become at writing formal mathematics, I think that it is no longer absurd to contemplate building an analogous library for some other ITP. I'm well aware of the risks of vibe-coded libraries; AI-generated Lean code is currently not high enough quality for Mathlib, and similarly we should not expect AI-generated Metamath code to be as good as Mathlib either. But I don't think we should dismiss the possibility for an alternative to Lean out of hand.
Let me also say that I am not advocating ditching Lean. It does have many excellent qualities, and the Lean community is a wonderful community that I don't wish to see destroyed. 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. But this would require some kind of institutional support, and I don't know where that would come from.