随着大模型在数学推理、可信计算、芯片设计验证等垂直领域的落地需求持续提升，高质量的形式化证明训练数据已成为行业公认的稀缺资源：由于形式化证明对逻辑严谨性要求极高，标注门槛远高于普通文本数据，此前公开领域缺少大规模、结构化的Lean 4格式定理证明数据集，制约了相关技术的落地进程。2026年5月19日，Multimodal Art Projection正式对外发布OProofs数据集，作为其OProver项目的核心组成部分，该数据集是目前公开领域规模最大的Lean 4格式定理证明数据集之一，一经上线便引发自动定理证明、形式化验证领域的广泛关注。
据公开信息显示，OProofs数据集总规模达6,804,694条记录，存储于73个经过zstd压缩的Parquet分片文件中，兼顾了存储空间效率与批量读取性能。每条记录包含四大核心字段：formal_statement对应Lean 4定理的形式化标准陈述、formal_proof为对应的可直接运行的Lean 4证明体，此外还提供可选的cot_proof链式思考推理文本与prompt生成提示，可满足不同场景下的模型训练、微调、评估需求。数据集标注语言为英语，采用商业友好的Apache-2.0许可协议，开发者无需开源衍生作品即可免费商用、修改与分发，大幅降低了学术研究与产业落地的使用门槛。该数据集专为定理证明、形式化数学和代码生成等任务设计，目前已首发上线HuggingFace平台。
从应用价值来看，OProofs数据集可为多个前沿领域提供核心数据支撑：在自动定理证明领域，基于该数据集训练的大模型可大幅提升复杂数学定理的推导准确率，辅助科研人员完成数学猜想的形式化验证，推动AI辅助基础数学研究的落地进程；在形式化验证领域，数据集可支撑面向软件、硬件的高可靠性验证模型研发，帮助芯片设计企业、金融核心系统开发商提升代码逻辑验证效率，降低安全漏洞风险；在代码生成领域，该数据集可用于训练高可信代码生成模型，为航空航天、医疗设备、工业控制等对代码可靠性要求极高的场景，提供可自动验证正确性的代码生成能力。
Dataset card内容：
Files and versions内容：
_1769672084863.jpg)