ExamFormal-Bench

ExamFormal-Bench is a Lean4 benchmark for formal proof generation, built from exam and competition problems across multiple academic levels. It covers six major domains — Analysis, Geometry, Algebra, Probability & Statistics, Computational Mathematics, and Discrete Mathematics — with 402 balanced test problems. Licensed under Apache 2.0.

ExamFormal-Bench 是一款面向形式化证明生成的 Lean4 基准测试集，构建自不同学术层级的考试与竞赛试题。该基准覆盖六大核心领域：分析学、几何学、代数学、概率论与统计学、计算数学以及离散数学，共包含402道分布均衡的测试题目。本数据集采用 Apache 2.0 开源许可协议授权发布。