CAM-Bench

CAM-Bench is a Lean-based benchmark for formal theorem proving in computational and applied mathematics.

Overview

This benchmark contains 778 exercises (1000 problems/sorries) in convex analysis, convex optimization, numerical optimization, and related matrix/vector calculus topics, collected from:

• Graduate-level textbooks in optimization and convex analysis,
• Course exercises and problem sets.

For users' convenience, we provide a JSON file where each entry represents a problem and includes the following information:

• Problem ID,
• Formal statement (Lean code),
• Natural language statement,
• Benchmark source (CAM-Bench),
• Source book, chapter, and exercise identifier,
• Problem type tags.

Benchmark Structure

Each Lean file is an independent exercise module. In practice, files may contain one or more formalized problem statements and can also include helper declarations used by those statements.

Typical contents include:

• Imports and scoped/open declarations at the beginning,
• One or more theorem statements with unfinished proofs marked by sorry,
• Optional helper declarations (for example def, structure, or namespace blocks),
• Natural language annotations preceding key statements when available.

Problem Distribution

The topic taxonomy of CAM-Bench is shown below.

Dataset Statistics

• Number of problems/sorries: 1000
• Number of benchmark exercises: 778
• Primary domains: convex optimization, numerical optimization, convex analysis, linear algebra, matrix analysis, proximal methods, duality

Lean Toolchain

This benchmark uses leanprover/lean4:v4.28.0. For each supported minor version of Lean, a corresponding updated iteration of the benchmark is available via the repository's tags.

License

See LICENSE for details. Third-party dependencies (e.g., mathlib) are distributed under their respective licenses.

Contact and Citation

We hope that the package is useful for your application. If you have any bug reports or comments, please feel free to email one of authors:

• Wentao Long, 23307130521@m.fudan.edu.cn
• Yunfei Zhang, zhangyunfei@qdu.edu.cn
• Chenyi Li, lichenyi@stu.pku.edu.cn
• Zaiwen Wen, wenzw@pku.edu.cn

If you find this repository useful, please consider citing our work:

@article{long2026cambench,
      title={CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean}, 
      author={Wentao Long and Yunfei Zhang and Chenyi Li and Li Zhou and Chumin Sun and Zaiwen Wen},
      year={2026},
      journal={arXiv preprint arXiv:2605.17255},
}