Euclean：在 Lean 中实现统一验证的自动化几何问题形式化

英文标题：Euclean: Automated Geometry Problem Formalization with Unified Verification in Lean

Euclean 提出了一套面向几何问题的自动化形式化方法，并在 Lean 中进行统一验证。论文指出，近期形式化推理系统已达到 IMO 级别表现，但代数和数论通常在 Lean 中处理，几何则仍依赖形式化保证有限的领域专用语言，生态较为割裂。该工作旨在弥合这一差距，为开发者提供可在 Lean 证明助手中验证的几何问题形式化路径，并推动数学推理系统向统一、可靠的验证框架发展。

2.1 KB 640 B 612 B 380 B 9.1 KB 32.7 KB 22.8 KB 24.2 KB 34.7 KB