数学界是否被困在Lean中？

Are We Stuck with Lean?

三年前，Lean 似乎只是众多证明助手中的一个选择，但如今它已占据主导地位。我提出疑问：是否有组织愿意支持 Lean 的替代品？Metamath 因其基于集合论和 Metamath Zero 的高正确性保障而成为有力竞争者。尽管 Lean 拥有 Mathlib 等强大生态，但其内核性能问题和类型论哲学争议仍存。随着 AI 生成形式化数学能力的提升，构建其他证明助手的库已不再遥不可及。我们不应因惯性而放弃探索更可靠、基于集合论的替代方案，这对整个数学社区至关重要。