ReasBook

English | 简体中文

ReasBook is a Lean 4 project for formalizing mathematics from textbooks and research papers. It preserves the structure of the original references while producing machine-checkable statements and proofs. Browse the generated documentation and project catalog to explore the current collection.

Many ReasBook projects are initialized with M2F and then checked and refined in Lean. You can also try Quokka, the public automated formalization system for turning long-form mathematical literature into compilable Lean 4 projects.

Toolchain Branches

main is the cross-version catalog. Source code stays on the registered version branches; the lightweight link folders below make each entry discoverable from this branch.

Registry status: Empty (not included in active releases) · Active (accepting PRs and included in release planning) · Frozen (kept, no new books) · Archived (historical only). Counts describe source directories and therefore may be nonzero on an Empty branch.

Main-branch Link Folders

Each directory in these indexes is a landing page for one book or paper. Open a directory and follow its prominent source link to the exact version branch and project folder.

• Books
• Papers
• Theorem dependency maps (the current Pages deployment contains TR-LALM)

Architecture

ReasBook separates versioned mathematical sources from cross-version tooling and generated output:

Generated sites, Lake artifacts, logs, and release state live outside the checkout under the configured cache root. Git history contains source and configuration, not generated sites. The immutable release and rollback model is recorded in ADR-0001.

Quick Start

Use the project catalog or the tables below to choose a formalization. Each entry records its exact version branch, source directory, and available documentation. Follow the matching branch link when you need to inspect or check the Lean source.

Download One Book with Git

Lean sources live on version branches. First find the book in the table below and note the version branch and directory shown by its source link. Git 2.25 or newer can use a sparse checkout to download that book without fetching the contents of every other book. For example, these commands download Analysis II from v4.30.0:

git clone --filter=blob:none --sparse --depth 1 --branch v4.30.0 --single-branch https://github.com/optpku/ReasBook.git ReasBook-Analysis2
cd ReasBook-Analysis2
git sparse-checkout set ReasBook/Books/Analysis2_Tao_2022
git branch --show-current
git sparse-checkout list

The final two commands should report v4.30.0 and ReasBook/Books/Analysis2_Tao_2022. To receive later commits on that version branch, run git pull --ff-only from the clone. For another title, replace the branch and directory with the exact values from its source link; paths are case-sensitive. The same procedure works for a paper by using its ReasBook/Papers/ path.

For local development, documentation generation, comparison, and static-site deployment, use the focused SDK guide for the relevant capability:

See the relevant SDK guide for operational commands. The homepage focuses on the project catalog.

Run the reading and review platform

ReasBook Reviewer is part of this repository. It serves books and papers from the existing SDK cache and supports signed-in review comments. From the repository root, with Python 3.11+:

python3.11 -m venv apps/reasbook-reviewer/.venv
apps/reasbook-reviewer/.venv/bin/python -m pip install -r apps/reasbook-reviewer/requirements.txt
export REASBOOK_CACHE_ROOT=/srv/reasbook-cache
apps/reasbook-reviewer/start_server.sh

Point REASBOOK_CACHE_ROOT at the cache you already built; no Lean compilation runs at server startup. Open . An empty cache shows pending indexes; sign-in is optional for reading and required for posting. The deployment guide covers Docker Compose, persistent comment storage and ReasLab authentication. GitHub Pages remains the static publication target; public comments require the reviewer backend.

Sponsors

• Beijing International Center for Mathematical Research, Peking University
• Great Bay University
• Huawei
• iQuest Research
• Sino-Russian Mathematics Center
• National Natural Science Foundation of China

Books

Titles open their catalog pages; version links open the Lean source directly.

Papers

Titles open their catalog pages; version links open the Lean source directly.

Open Questions Resolved by Our Team

The following papers present our team’s solutions to previously open research questions.

Other Formalized Papers

Contributing

See CONTRIBUTING.md for the human-facing contribution procedure. Agent-assisted contributions can follow the ReasBook contributing skill, which encodes the branch, metadata, validation, and pull-request rules.

• Book and paper code lives on the registered version branch matching its Lean/mathlib toolchain; only registered stable vX.Y.Z versions are accepted.
• Book and paper code is not merged to main. main remains the cross-version catalog, while its link folders point to the corresponding version branches.
• PR base, PR title version, ReasBook/lean-toolchain, and book metadata (when applicable) must all match.

Lean Projects

Publications

Mathematical Formalization

• Wanli Ma, Zichen Wang, Zaiwen Wen, A Unified Framework for Formalizing Matrix Decomposition Proofs. (Paper)
• Chenyi Li, Ziyu Wang, Wanyi He, Yuxuan Wu, Shengyang Xu, Zaiwen Wen. Formalization of Complexity Analysis of the First-order Optimization Algorithms, Journal of Automated Reasoning. (Paper)
• Chenyi Li, Zichen Wang, Yifan Bai, Yunxi Duan, Yuqing Gao, Pengfei Hao, Zaiwen Wen. Formalization of Algorithms for Optimization with Block Structures, Science in China Series A: Mathematics. (Paper)
• Chenyi Li, Shengyang Xu, Chumin Sun, Li Zhou, Zaiwen Wen. Formalization of Optimality Conditions for Smooth Constrained Optimization Problems. (Paper)
• Chenyi Li, Zaiwen Wen. An Introduction to Mathematics Formalization Based on Lean. (Paper)

Autoformalization and Automated Theorem Proving

• Wentao Long, Yunfei Zhang, Chenyi Li, Zaiwen Wen, MECA: A Mechanism-Centered Agent for Constructing Well-Specified and Valuable Mathematical Conjectures. (Paper)
• Chenyi Li, Yanchen Nie, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen. OptProver: Bridging Olympiad and Optimization through Continual Training in Formal Theorem Proving, ICML 2026. (Paper)
• Zichen Wang, Wanli Ma, Zhenyu Ming, Gong Zhang, Kun Yuan, Zaiwen Wen. M2F: Automated Formalization of Mathematical Literature at Scale. (Paper)
• Ziyu Wang, Bowen Yang, Chenyi Li, Yuan Zhang, Shihao Zhou, Bin Dong, Zaiwen Wen. Translating Informal Proofs into Formal Proofs Using a Chain of States. (Paper)
• Chenyi Li, Wanli Ma, Zichen Wang, Zaiwen Wen. SITA: A Framework for Structure-to-Instance Theorem Autoformalization, AAAI 2026. (Paper)

Theorem-Proof Checking

• Ziyu Wang, Qiming Dai, Yishan Wu, Zaiwen Wen. FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence.
• Ziyu Wang, Qiming Dai, Chenyi Li, Zaiwen Wen, Beyond Formal Correctness: Structure-Aware Evaluation of Informal–Formal Proof Correspondence

Premise Selection

• Zichen Wang, Anjie Dong, Zaiwen Wen. Tree-Based Premise Selection for Lean4, NeurIPS 2025. (Paper)
• Shu Miao, Zichen Wang, Anjie Dong, Yishan Wu, Weixi Zhang, Zaiwen Wen. Directed Multi-Relational GCNs for Premise Selection.

Benchmark

• Bowen Yang, Yi Yuan, Chenyi Li, Ziyu Wang, Liangqi Li, Bo Zhang, Zhe Li, Zaiwen Wen. Construction-Verification: A Benchmark for Formalizing Applied Mathematics in Lean 4. (Paper)
• Wentao Long, Yunfei Zhang, Chenyi Li, Li Zhou, Chumin Sun, Zaiwen Wen. CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean. (Paper)

Contributors

• Chenyi Li, School of Mathematical Sciences, Peking University, China ([email protected])
• Wanli Ma, Beijing International Center for Mathematical Research, Peking University, China ([email protected])
• Zichen Wang, School of Mathematical Sciences, Peking University, China ([email protected])
• Ziyu Wang, School of Mathematical Sciences, Peking University, China ([email protected])
• Zaiwen Wen, Beijing International Center for Mathematical Research, Peking University, China ([email protected])
• Yifan Bai, Anjie Dong, Yunxi Duan, Xinyi Guo, Pengfei Hao, Yuhao Jiang, Gongxun Li, Yantao Li, Wentao Long, Zebo Liu, Zhenxi Liu, Siyuan Ma, Guangxuan Pan, Siyuan Shao, Weiran Shi, Junren Si, Xuran Sun, Xuan Tang, Feiming Wang, Yijie Wang, Zhiyan Wang, Zixi Wang, Suwu Wu, Mingyue Xu, Lurong Yang, Yunfei Zhang, Jian Yu, Changyun Zou

Citation

If you use ReasBook, please cite both the M2F paper and the repository:

M2F paper:

@misc{wang2026m2f,
  author        = {Zichen Wang and Wanli Ma and Zhenyu Ming and Gong Zhang and
                   Kun Yuan and Zaiwen Wen},
  title         = {{M2F}: Automated Formalization of Mathematical Literature at Scale},
  year          = {2026},
  eprint        = {2602.17016},
  archivePrefix = {arXiv},
  primaryClass  = {cs.AI},
  doi           = {10.48550/arXiv.2602.17016},
  url           = {https://arxiv.org/abs/2602.17016}
}

ReasBook software:

@software{reasbook2026,
  author  = {{ReasBook Contributors}},
  title   = {{ReasBook}: Formalizations of Mathematical Textbooks and
             Research Papers in {Lean 4}},
  year    = {2026},
  url     = {https://github.com/optpku/ReasBook},
  license = {Apache-2.0}
}

When referring to a particular formalization, also cite the original book or paper and record the ReasBook project directory, version branch, and full commit SHA. For example: v4.30.0, ReasBook/Books//, and the output of git rev-parse HEAD. This repository also provides CITATION.cff for citation tools and GitHub’s citation interface.

License

ReasBook uses the Apache License 2.0, matching mathlib. Unless an individual file carries a different notice, this license covers ReasBook content on every official branch and in all copies and forks derived from this repository. Fork-specific additions and third-party dependencies remain subject to their respective license notices.