LiveLeanTriathlon

github2026-05-29 更新2026-06-04 收录

定理自动证明

形式化验证

数据链接：

https://github.com/project-numina/LeanTriathlon 数据链接链接失效反馈

官方服务：

资源简介：

LiveLeanTriathlon是一个用于Lean 4中自动定理证明和自动形式化的基准套件，包含用Lean 4形式化的数学定理集合、证明中使用的支持引理的形式化，以及以LaTeX蓝图形式提供的这些定理、引理及其证明的非正式描述。这些定理来自多个来源，覆盖多个数学领域。

LiveLeanTriathlon is a benchmark suite for automated theorem proving and automated formalization in Lean 4. It contains a collection of mathematical theorems formalized in Lean 4, formalizations of supporting lemmas used in their proofs, as well as informal descriptions of these theorems, lemmas and their proofs provided in the form of LaTeX blueprints. These theorems originate from multiple sources and cover a wide range of mathematical fields.

创建时间：

2026-05-24

原始信息汇总

数据集概述

数据集名称：LiveLeanTriathlon

数据集地址：https://github.com/project-numina/LeanTriathlon

数据集描述：LiveLeanTriathlon 是一个基准测试集，专为在 Lean 4 中的自动化定理证明和自动形式化而设计。它包含一系列在 Lean 4 中形式化的数学定理，以及这些定理证明中使用的支持引理的形式化，并附带这些定理、引理及其证明的非形式化描述（以 LaTeX 蓝本形式提供）。这些定理来源于多种资料，包括 1000+ 定理项目、个人贡献者的扩展项目以及其他数学文献，覆盖了多个数学领域。

数据集目标

评估自动化定理证明系统在 Lean 4 中处理多样化定理集的能力，该集比以往侧重于竞赛数学的基准测试更多样，更接近研究级数学。
为自动形式化系统提供测试平台，使其能够将定理和引理的非形式化描述转换为 Lean 4 中的形式化陈述。
探索利用人机协作来协助更大规模形式化项目的方法。

数据构成

定理来源：包括 1000+ 定理项目、个人贡献者的扩展项目以及其他数学文献。
覆盖领域：涵盖多个不同的数学领域。
数据集内容：
- 每个定理的目录包含：
  - All.lean：包含主要定理陈述（已用 sorry 占位）。
  - 其他相关文件（如 MainTheorem.lean、BackgroundLemmas.lean）已从公开版本中移除，以防止数据泄漏。
- LiveLeanTriathlonSorry/Mathlib/：包含所需的但未在 mathlib 中出现的引理。
数据统计：theorem_stats.json 文件包含关于定理的统计信息，如按 AMS 分类的计数、哪些定理拥有完整形式化证明、非形式化证明或背景引理陈述等。

数据变体与基准 JSONL

数据集提供了两种目录变体和三种 JSONL 文件，用于评估：

目录变体（通过 scripts/create_sorries/create_sorries.py 生成）：
- LiveLeanTriathlonSorry/：将每个 theorem/lemma 的证明替换为 := by sorry。
- LiveLeanTriathlonSorryNoLemmas/：仅将 @[AMS] 标记的主定理保留 := by sorry，辅助引理被降级为 axiom，使每个非 Mathlib 文件夹只暴露一个开放目标。
JSONL 文件（通过 scripts/create_sorries/create_statement_jsonl.py 生成）：
- statement.jsonl：每行对应一个 theorem/lemma，包含其代码（项目中前序证明已替换为 sorry）。
- statements_hard.jsonl：每行对应一个 @[AMS] 定理，包含其代码，同一文件中的其他 @[AMS] 定理作为 axiom，目标用 sorry。
- statements_autoformalization.jsonl：每行对应一个 @[AMS] 定理，包含其代码（仅目标用 sorry），并额外包含 title、informal_statement 和 informal_proof 字段，这些信息从对应的 LaTeX 蓝本文件中提取。

JSONL 基本模式： json {"project_name": "...", "name": "...", "type": "theorem"|"lemma", "code": "..."}

对于 statement.jsonl 中包含项目本地导入的行，会额外添加 imported_file 字段，包含传递性的兄弟文件内容（证明已替换为 sorry，文件间用 -- File: <module> 标记分隔）。
statements_autoformalization.jsonl 额外包含 title、informal_statement 和 informal_proof 字段。

许可证

软件：基于 Apache License, Version 2.0 (Apache-2.0) 许可。
内容：可能包含第三方内容，其许可协议如下：
- 来自维基百科和 MathOverflow 的材料：Creative Commons Attribution-Share-Alike License 4.0。
- 来自 Stacks Project 的材料：GNU Free Documentation License。
- 来自 arXiv 的材料：根据相关论文的许可协议。

搜集汇总

数据集介绍

构建方式

在自动定理证明与自动形式化研究领域，现有基准测试大多聚焦于竞赛数学，难以反映科研级数学的复杂性。为此，LiveLeanTriathlon数据集应运而生，它是一套基于Lean 4定理证明器构建的基准测试集。该数据集从1000+定理项目、个体贡献者扩展项目及其他数学文献中精选定理，覆盖多个数学分支。构建时，仓库为每个定理设立独立目录，包含经过'抱歉'处理的主定理陈述（即使用`sorry`占位符替换证明），并剔除了非形式化与形式化证明，以防数据泄露。此外，通过脚本自动生成两种目录变体：一种将所有定理和引理的证明替换为`sorry`，另一种仅对主定理保留`sorry`并将辅助引理降级为公理，同时生成扁平的JSONL文件，每行代表一个独立的证明或形式化问题。

特点

该数据集的核心特点在于其多样性与科研相关性。与以往偏重竞赛数学的基准不同，LiveLeanTriathlon的定理来源广泛，涵盖代数、几何、分析等多个数学领域，更接近真实的研究级数学场景。它特别设计了两种变体（完整引理版与仅主定理版），以灵活评估自动定理证明系统在不同引理支持下的能力。同时，数据集为每个定理提供了LaTeX蓝图形式的非形式化描述，支持自动形式化系统的测试。每行JSONL问题均包含独立的代码片段，去除了项目内导入和装饰器，方便直接评估，其中自动形式化子集还额外提供了标题、非形式化陈述与证明，便于多维度评测。

使用方法

用户可通过两种方式使用该数据集。其一，利用目录变体进行构建与评估：运行`python3 scripts/create_sorries/create_sorries.py`生成`LiveLeanTriathlonSorry/`或`LiveLeanTriathlonSorryNoLemmas/`目录，然后使用`lake build`命令构建对应的Lean库，即可在Lean环境中测试自动定理证明系统。其二，使用JSONL文件进行批量评估：运行`python3 scripts/create_sorries/create_statement_jsonl.py`生成`statement.jsonl`、`statements_hard.jsonl`和`statements_autoformalization.jsonl`三个文件，每行代表一个独立问题，包含项目名称、定理名称、类型及去除了项目内依赖的代码。对于自动形式化任务，`statements_autoformalization.jsonl`还提供了非形式化描述，用户可据此训练或测试模型将自然语言数学陈述转换为Lean 4的形式化代码。

背景与挑战

背景概述

LiveLeanTriathlon数据集由Project Numina团队于2025年创建，旨在评估和推动自动化定理证明（ATP）与自动形式化（autoformalization）系统在Lean 4证明助手中的能力。该数据集精心收集了来自“1000+定理项目”、个人贡献者扩展及数学文献的众多数学定理，覆盖多个数学分支，其核心研究问题在于构建一个比以往偏重竞赛数学的基准更加多样、更贴近研究级数学的测试平台。通过提供定理的Lean 4形式化表述、支撑引理及相应的LaTeX蓝图，LiveLeanTriathlon不仅为评估ATP系统的性能提供了丰富素材，也为人机协作辅助大规模形式化项目探索了新的路径，对形式化数学与人工智能交叉领域具有重要影响力。

当前挑战

LiveLeanTriathlon面临的主要挑战源于其双重视角：首先，在领域问题上，自动化定理证明系统需要处理涵盖广泛数学领域、复杂度接近研究水平的定理，这与传统竞赛数学问题不同，对系统的推理深度和领域泛化能力提出了更高要求；同时，自动形式化系统须能准确理解非正式的LaTeX描述并生成正确的形式化代码，这对自然语言到形式语言的语义转换构成了巨大考验。其次，在构建过程中，数据集面临数据泄露防范的挑战，需剥离正式与非正式证明以构建可靠的基准；此外，还需妥善处理来自多个第三方来源（如Wikipedia、arXiv）内容的版权合规问题，并确保不同来源的定理在统一的Lean 4框架下保持一致的形式化标准。

常用场景

经典使用场景

在数学定理机器证明与自动形式化研究领域，LiveLeanTriathlon基准测试套件为评估和提升自动化定理证明系统在Lean 4环境中的能力提供了关键工具。其核心使用场景包括：作为多样化定理集合的测试平台，评估定理证明系统处理远超竞赛数学范畴、更贴近研究级数学问题的能力；为自动形式化系统提供从非正式定理描述生成Lean 4形式语句的试验场；以及探索人类与人工智能协作以辅助大规模形式化项目的新途径，从而推动形式化验证技术在数学研究中的深度应用。

衍生相关工作

该数据集衍生了一系列聚焦于定理证明与自动形式化的经典工作，包括基于其sorried变体（如LiveLeanTriathlonSorry和LiveLeanTriathlonSorryNoLemmas）开发的评估流程，用以测试定理证明系统在提供或不提供辅助引理支持下的表现；以及从语句JSONL衍生出的基准任务，如statement.jsonl用于单目标证明评估，statements_hard.jsonl用于无引理支撑的硬核定理证明，statements_autoformalization.jsonl则专门用于非正式陈述到形式语句的自动形式化任务。这些衍生工作共同构建了从基础证明到自动形式化的立体化评估体系，推动了Lean 4生态中人工智能辅助证明技术的系统化研究。

数据集最近研究