formal-math-autoformalization

Formal Math Autoformalization Dataset（形式数学自动形式化数据集）是一个由Agentic Commons网络创建的开源数据集，专门用于数学自动形式化任务。该数据集包含自然语言描述的数学陈述与经过严格验证的Lean 4定理证明形式化代码的配对。每个数据对在发布前都通过了双重验证：1) 编译验证，确保Lean 4代码能在指定工具链和Mathlib版本下成功编译，且证明不含未完成项，仅依赖允许的内核公理；2) 忠实性验证，通过LLM批评者模型将形式化陈述回译成自然语言，判断是否忠实地捕获原始语义。数据集采用JSON Lines格式存储，每个样本包含18个字段，记录自然语言陈述、Lean 4定理签名、证明体、使用的Mathlib概念、验证级别、忠实性评分、贡献者信息、来源、许可证（CC0-1.0）及编译环境等元数据。数据集规模较小（小于1K样本），当前版本偏向于本科难度的数学陈述，主要适用于文本生成任务，特别是自动形式化、代码生成、定理证明以及数学自然语言理解与形式语言转换模型的训练或评估。Formal Math Autoformalization Dataset is an open-source dataset created by the Agentic Commons network, specifically tailored for mathematical autoformalization tasks. This dataset consists of pairs of natural language-described mathematical statements and rigorously verified formalized code for Lean 4 theorem proving. Each data pair undergoes dual validation prior to release: 1) Compilation validation: ensuring that the Lean 4 code can be successfully compiled under the specified toolchain and Mathlib version, with no incomplete proof steps and only relying on permitted kernel axioms; 2) Faithfulness validation: translating the formalized statement back into natural language using an LLM-based critic model to verify whether it faithfully captures the original semantics. The dataset is stored in JSON Lines format, with each sample containing 18 fields that record metadata including natural language statements, Lean 4 theorem signatures, proof bodies, utilized Mathlib concepts, validation levels, faithfulness scores, contributor information, sources, license (CC0-1.0), and compilation environments. The dataset is small-scale with fewer than 1,000 samples. The current version focuses on mathematical statements at undergraduate-level difficulty, and is primarily applicable to text generation tasks, particularly the training or evaluation of models for autoformalization, code generation, theorem proving, and mathematical natural language understanding and formal language translation.

原始信息汇总

数据集概述

数据集名称：Formal Math Autoformalization Dataset

数据集来源：由 Agentic Commons 网络生成。

许可协议：CC0-1.0（公共领域奉献）。

语言：英语（en）。

任务类别：文本生成（text-generation）。

数据集规模：少于 1,000 条样本（n<1K）。

配置：

• 默认配置（default），包含训练集（train），数据文件路径为 data/formal_math.jsonl。

---

数据内容与结构

每条数据为 JSON 格式（每行一个 JSON 对象），包含以下字段：

字段	类型	描述
submission_marker	字符串	公共 ACG 提交标记（sm_xxxxxxxx），是每行的稳定贡献 ID 和主键。
acg_url	字符串	解析器链接（https://agentic-commons.org/s/{submission_marker}），打开公共归属页面。
contributor_handle	字符串	null
nl_statement	字符串	自然语言数学陈述。
lean4_statement	字符串	Lean 4 theorem … 签名（不含证明）。
lean4_proof	字符串	Lean 4 证明体（:= by …）。
mathlib_concepts	字符串数组	所使用的 Mathlib 概念/引理。
verification_level	字符串	验证结果（compile+nli-pass 或 kernel-proven）。
lean_compiles	布尔值	是否编译通过（此处始终为 true）。
axioms_used	字符串数组	证明依赖的内核公理（仅包含白名单中的公理）。
nli_score	浮点数	忠实性评判模型的置信度（0–1）。
backtranslation	字符串	评判模型将 Lean 陈述回译的自然语言版本。
judge_model	字符串	忠实性评判模型名称。
difficulty_tier	字符串	null
provenance	字符串	自然语言陈述的来源（如 synthesized）。
license	字符串	每行许可（CC0-1.0）。
mathlib_revision	字符串	证明所依赖的 Mathlib 提交版本。
lean_toolchain	字符串	证明所依赖的 Lean 工具链。

---

验证机制

每对（自然语言陈述 + Lean 4 形式化证明）通过以下两道关卡后才被发布：

1. 编译门（确定性）：Lean 4 陈述 + 证明必须在固定版本的 Mathlib 下离线编译通过。证明必须完整，不允许使用 sorry/admit，且内核公理必须在白名单 {propext, Classical.choice, Quot.sound} 内（禁止通过 native_decide 等途径引入隐藏公理）。
2. 忠实性门（LLM 评判）：由第二个模型将 Lean 陈述回译为自然语言，并判断其是否忠实捕捉原始陈述的含义（相同的一般性——自由变量被全称量化）。仅通过忠实性检查的对才发布。

verification_level 字段记录验证结果：

• compile+nli-pass：编译通过 且 被评判为忠实（已发布）。
• kernel-proven：编译通过，经过内核检查（保留用于未来更严格的层级，已发布）。
• compile-only：编译通过但忠实性未确认（从不发布）。

---

技术细节

• Lean 工具链：leanprover/lean4:v4.30.0
• Mathlib 版本：c5ea00351c28e24afc9f0f84379aa41082b1188f（v4.30.0）
• 复现验证方法：使用指定版本的 elan 安装 Lean 工具链，在对应 Mathlib 签出版本下，将 Lean 陈述和证明嵌入 import Mathlib 的脚本中，用 lake env lean 编译，并通过 #print axioms 检查公理白名单。

---

局限性

• 忠实性由 LLM 评判，而非人工；nli_score 是模型置信度，并非 NL ↔ Lean 完美对应的正式保证。
• 须使用固定的 Mathlib/Lean 版本才能复现编译，在其他版本上不保证编译通过。
• 早期发布版本较小，且偏向本科水平陈述。

---

引用信息

建议引用格式：

Agentic Commons (2026). Formal Math Autoformalization Dataset [Data set]. https://huggingface.co/datasets/AgenticCommons/formal-math-autoformalization

BibTeX：

bibtex @misc{agenticcommons_formalmath_2026, title = {Formal Math Autoformalization Dataset}, author = {{Agentic Commons}}, year = {2026}, howpublished = {Hugging Face Hub}, url = {https://huggingface.co/datasets/AgenticCommons/formal-math-autoformalization}, note = {Pinned to Mathlib v4.30.0 / Lean leanprover/lean4:v4.30.0} }

首个版本快照存档至 Zenodo 后将提供 DOI（待定）。

搜集汇总

数据集介绍

构建方式

该数据集由Agentic Commons网络社区精心构建，汇聚了自然语言数学命题与其对应的Lean 4形式化证明。每一对数据的收录均需通过两项严苛的验证关卡：其一是编译门控，确保Lean 4语句与证明在锁定的Mathlib工具链上能零缺陷地编译通过，杜绝任何‘sorry’或‘admit’占位符，并仅允许经过核准的内核公理；其二是忠实度门控，借助大语言模型将Lean语句反向翻译为自然语言，评判其是否精确捕捉原始命题的普遍性内涵。唯有同时通过两项检验的数据，方被收录于数据集中。

特点

本数据集具备高度的可靠性与可复现性。每条记录均包含完整的元数据，如提交标识符、贡献者信息、自然语言陈述、Lean 4定理签名与证明体、所使用的Mathlib概念、验证等级、忠实度评分以及反向翻译文本等。数据集采用CC0-1.0公共领域许可，鼓励广泛传播与再利用。目前收录的条目规模虽小，但聚焦于本科水平的数学命题，为自动形式化研究提供了高质量的基准数据。

使用方法

使用本数据集时，研究者可加载JSONL格式的数据文件，每条记录为一个独立的JSON对象。数据可直接用于训练或评估自动形式化系统。要复现编译验证，需安装指定的Lean工具链‘leanprover/lean4:v4.30.0’，并切换至对应的Mathlib修订版。将Lean语句与证明拼接成Lean文件后，使用‘lake env lean’命令编译，并可利用‘#print axioms’检查所用公理是否在白名单内。该方法适用于批量验证及基准测试。

背景与挑战

背景概述

形式化数学验证是人工智能与定理证明交叉领域的核心议题，其目标在于将自然语言描述的数学命题转化为机器可检查的形式化证明。2026年，Agentic Commons网络发布了Formal Math Autoformalization数据集，旨在为自动形式化研究提供高质量的平行语料。该数据集以Lean 4证明助手为后端，锚定mathlib v4.30.0版本，每一条自然语言-形式化语句对均通过编译验证和LLM驱动的忠实性审查，确保了数据的严谨性与可靠性。作为公开领域（CC0-1.0）资源，它已成为推动autoformalization方法发展、评估大语言模型数学推理能力的权威基准，显著降低了形式化研究的入门门槛。

当前挑战

该数据集面临的核心挑战来自两个层面：其一，在领域问题层面，自然语言数学命题的歧义性与形式化表达的精确逻辑之间存在天然鸿沟，LLM评判的忠实性检验虽能过滤明显偏差，却无法完美保证语义等价，且当前规模仅数百条，覆盖范围局限于本科层次数学，难以支撑复杂数学理论的自动形式化需求。其二，在构建过程中，每条数据需严格依赖固定Lean 4工具链与mathlib版本编译，版本锁定策略虽保障了可复现性，却导致数据缺乏版本迁移兼容性；同时，贡献者需手动编写通过双重检验的证明体，人工成本高昂，限制了数据集的快速增长与多样化扩展。

常用场景

经典使用场景

在数学定理的自动形式化领域，该数据集通过提供成对的自然语言数学表述与经过机器校验的Lean 4形式化证明，为训练和评估自动形式化系统提供了高质量的基准。研究者可借助这些数据，开发将非形式化数学文本转化为严格形式化语言的模型，特别适用于大语言模型在数学推理和形式化验证方面的微调与评估。每条数据都经过编译门和忠实度门的双重验证，确保了自然语言与Lean代码之间的语义一致性，从而为形式化系统的构建提供了可靠的数据支撑。

衍生相关工作

该数据集的发布催生了一系列自动形式化领域的重要工作。其设计理念启发了基于LLM的自动形式化系统研究，例如将大语言模型与形式验证工具链结合，形成端到端的自然语言到定理证明代码的生成流水线。数据集中明确的编译和忠实度评价标准，也促使后续研究开发更精确的语义等价性度量指标和对抗性验证策略。此外，该数据集的方法论被借鉴用于构建跨语言的数学形式化语料库，推动数学知识在多个定理证明器之间的互操作性和可迁移性研究。

数据集最近研究

最新研究方向

该数据集聚焦于数学形式化与自动形式化的前沿探索，通过构建自然语言数学命题与Lean 4形式化证明的精准配对，为机器辅助数学推理和可验证数学研究提供了关键资源。其独特的双层验证机制——编译门控与基于LLM的回译忠实度检测——确保了数据的高可靠性，直接回应了当前形式化数学中普遍存在的正确性与语义对齐挑战。与数学界借助Lean 4和Mathlib库推动的“数学蓝图”项目及形式化验证热潮相呼应，该数据集不仅支撑了自动定理证明与数学文本理解的交叉研究，更推动了形式化数学在本科教育、数学出版以及智能辅导系统等场景中的落地应用，展现了从理论推导到工程验证的闭环意义。