430道代数题形式化入库，助力数学AI推理研究
Lean-GAP: A Dataset of Formalized Graduate Algebra Problems
- 从教材提取题目，用Lean 4自动形式化并验证对应关系
- 构建首个系统化研究生代数题形式化数据集，含430题
- 揭示形式化难点，适合数学与AI交叉研究者参考
我们提出Lean-GAP（Lean-Graduate Algebra Problems），基于《抽象代数》（Dummit and Foote）教材整理出430道研究生级代数问题的形式化版本。通过建立可扩展的流水线——包括PDF转LaTeX预处理、自动形式化至Lean 4、以及非形式化与形式化内容的验证——完成数据构建。尽管预处理和自动形式化可高度自动化，但验证环节仍需人工细致审校，最为耗时。本工作贡献包括：(i) 构建结构化形式化习题数据集；(ii) 提出系统化的教材数学形式化方法；(iii) 分析形式化过程中的常见挑战。同时对比不同自动形式化模型表现，指出现有技术在将非形式化表述转化为正式语言时的关键瓶颈。
原文摘要 · Abstract (English)
We present Lean-GAP (Lean-Graduate Agebra Problems), 430 formalized graduate-level algebra problems from the textbook Abstract Algebra by Dummit and Foote. We develop a scalable pipeline consisting of PDF-to-LaTeX preprocessing, autoformalization into Lean 4, and verification of informal-formal correspondence. While the preprocessing and autoformalization stages can be largely automated, we find that verification remains the most subtle and labor-intensive component, requiring careful human oversight. Our contributions include (i) the construction of a structured dataset of formalized exercises, (ii) a systematic methodology for formalizing textbook mathematics, and (iii) an analysis of recurring challenges in the formalization process. We also compare the performance of different autoformalization models and highlight key bottlenecks in translating informal statements into formal language.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。