LeanEuclid
收藏arXiv2025-09-30 收录
下载链接：
https://github.com/loganrjmurphy/LeanEuclid
下载链接
链接失效反馈官方服务：
资源简介：
该数据集是一个自动形式化基准测试，它结合了来自欧几里得《几何原本》中的问题和在Lean证明助手中正式化的UniGeo数据集。该数据集不仅包含了欧几里得《几何原本》中的非正式证明，还包括了UniGeo数据集中的问题，这些内容被用于评估大型语言模型在自动形式化几何定理陈述方面的表现。
This dataset is an automated formalization benchmark that integrates problems from Euclid's Elements and the UniGeo dataset formalized within the Lean proof assistant. It encompasses both the informal proofs from Euclid's Elements and the problems contained in the UniGeo dataset, and is utilized to evaluate the performance of large language models (LLMs) in the task of automated formalization of geometric theorem statements.
提供机构：
Lean proof assistant community
