8 hours ago
- 三年前，作者在一次演讲中提出，数学界对选择证明助手的窗口期很窄，Lean 正在获得发展势头，但尚未成为必然。
- 核心问题是，是否有组织会认真支持 Lean 的替代品，例如 Metamath。
- Metamath 有两个优势：由于 Metamath Zero，它提供了更高的可靠性保证；以及一个集合论基础，解决了对“命题即类型”哲学的担忧。
- Lean 的流行可能更多是由知名人物推动，而非其客观优越性；其主要优势在于 Mathlib 库。
- 人工智能在形式数学方面的进展使得为其他证明器构建类似库变得可行，尽管质量仍然是一个挑战。
- 作者主张为社区的利益提供一个可行的 Lean 替代品，但这需要机构支持，而其来源尚不明确。