Lean への依存は避けられないのか？代替証明支援体の可能性

Are We Stuck with Lean?

私は数学界が Lean への依存を脱却できるかどうかを問う。Lean は現在主流だが、Metamath のような集合論ベースの代替案は、AI 生成証明の検証においてより高い安全性を提供する可能性がある。AI の進歩により、Mathlib に匹敵するライブラリを他のシステムで構築することも現実的になりつつある。