Goedel v2

新框架在 Lean 中自动化几何问题形式化

研究人员开发了 Euclean，一个旨在 Lean 证明助手内自动化几何问题形式化的新框架。该系统通过使几何问题能够以原生的 Mathlib（Lean 的标准库）表示，解决了代数和几何推理系统之间的碎片化问题。Euclean 构建了大型数据集 OMNI-Geometry 和 Numina-Geometry，包含超过 178,000 个几何问题，这些数据集已证明能提高神经定理证明模型的性能。