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.
| Branch | Lean/mathlib | Registry status | Books/Papers |
|---|---|---|---|
v4.32.0 |
v4.32.0 |
Empty | 1 / 2 |
v4.32.2 |
v4.32.2 |
Active | 0 / 2 |
v4.30.0 |
v4.30.0 |
Active | 9 / 2 |
v4.26.0 |
v4.26.0 |
Active | 4 / 2 |
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.
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)
ReasBook separates versioned mathematical sources from cross-version tooling and generated output:
| Path | Responsibility |
|---|---|
ReasBook/ |
Lean sources on their matching version branches |
ReasBookWeb/ |
Verso site shell and catalog generation |
apps/reasbook-reviewer/ |
Public reading, source/docs/graph inspection and authenticated review comments |
sdk/ |
Reusable build, Verso, theorem-graph, comparator, and deployment APIs |
scripts/ |
Thin repository-specific build and Pages adapters |
config/ |
Toolchain registry, canonical versions, release profiles, and schemas |
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.
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.
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 listThe 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/<directory> path.
For local development, documentation generation, comparison, and static-site deployment, use the focused SDK guide for the relevant capability:
| Capability | Guide |
|---|---|
| Lean build and reachable project documentation | Build SDK |
| Verso site and literate pages | Verso SDK · upstream Verso |
| Theorem dependency maps | Theorem graph SDK |
| Challenge/Solution comparison | Comparator SDK · upstream Comparator |
| Multi-stage deployment and release assembly | Deploy SDK |
See the relevant SDK guide for operational commands. The homepage focuses on the project catalog.
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.shPoint REASBOOK_CACHE_ROOT at the cache you already built; no Lean compilation
runs at server startup. Open http://127.0.0.1:8876/ReasBook/. 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.
- Beijing International Center for Mathematical Research, Peking University
- Great Bay University
- Huawei
- iQuest Research
- Sino-Russian Mathematics Center
- National Natural Science Foundation of China
Titles open their catalog pages; version links open the Lean source directly.
| Formalization | Source | Contributors | Resources |
|---|---|---|---|
| A Concise Course in Algebraic Topology J. Peter May (1999) |
v4.30.0 |
Ze Yuan, Zichen Wang | Docs | Verso |
| Analysis II Terence Tao (4th ed., 2022) |
v4.26.0v4.30.0 |
9 contributorsChenyi Li, Min Cui, Qiming Dai, Shu Miao, Wanli Ma, Yi Yuan, Zichen Wang, Ziyu Wang, Zaiwen Wen |
Docs | Verso |
| Combinatorial Group Theory Magnus, Karrass, and Solitar (2004) |
v4.30.0 |
Zichen Wang | Docs | Verso |
| Convex Analysis R. Tyrrell Rockafellar (1970) |
v4.26.0 |
21 contributorsChangyu Zou, Chenyi Li, Guangxuan Pan, Pengfei Hao, Qiming Dai, Shu Miao, Siyuan Shao, Suwu Wu, Wanli Ma, Weiran Shi, Xinyi Guo, Xuran Sun, Yifan Bai, Yijie Wang, Yunfei Zhang, Yunxi Duan, Yuhao Jiang, Zebo Liu, Zhiyan Wang, Zichen Wang, Zaiwen Wen |
Docs | Verso |
| Convex Analysis and Monotone Operator Theory in Hilbert Spaces Bauschke and Combettes (2nd ed., 2017) |
v4.30.0 |
Yifan Bai, Zichen Wang, Zaiwen Wen | Docs | Verso |
| First-Order Methods in Optimization Amir Beck (2017) |
v4.30.0 |
Shu Miao, Zichen Wang, Zaiwen Wen | Docs | Verso |
| Integer Programming Conforti, Cornuejols, and Zambelli (2014) |
v4.26.0 |
38 contributorsBinghe Huang, Chenglin Li, Chenrui Yang, Chenxi Liu, Congyuan Lei, Dongye Song, Fuzhi Wang, Haodong Zhang, Jiangnan Song, Jinmin Song, Junze Qiao, Junzhe Lai, Kaiwen He, Liming Han, Lurong Yang, Meng Zhou, Pengqi Lei, Renran Luo, Siyan Chen, Wangqi Liu, Wenxin Zeng, Wanli Ma, Wenxuan Wu, Xinru Zhu, Xu Han, Xutianshi Tao, Yichao Guo, Youyou Qin, Yuhan Zhang, Yushen Guo, Yutong Zhang, Ze Zhai, Zheng Ma, Zhiyong Chen, Zichen Wang, Zichen Xu, Zihao Liu, Zaiwen Wen |
Docs | Verso not published |
| Introduction to Real Analysis, Volume I Jiri Lebl (v6.2, 2025) |
v4.26.0v4.30.0 |
Zichen Wang, Zaiwen Wen | Docs | Verso |
| Introductory Lectures on Convex Optimization Yurii Nesterov (2004) |
v4.30.0 |
Chenyi Li, Siyuan Shao, Yijie Wang, Feiming Wang, Weiran Shi, Yuhao Jiang, Zebo Liu, Wentao Long | Docs | Verso |
| Optimization Theory and Methods: Nonlinear Programming Wenyu Sun and Ya-xiang Yuan (2006) |
v4.30.0 |
Chenyi Li, Wanli Ma, Zichen Wang | Docs | Verso |
| Probability Theory: A Comprehensive Course Achim Klenke (3rd ed., 2020) |
v4.29.0 |
Xuanzhi Ren, Zichen Wang | Source only (excluded from the current release profile) |
| Lectures on Riemann Surfaces Otto Forster (1981) |
v4.30.0 |
Zichen Wang | Docs | Verso |
| Computational Methods for Inverse Problems Curtis R. Vogel (2002) |
Not assigned to an active release branch | Yifan Bai, Wanli Ma, Zichen Wang | Source only (excluded from the current release profile) |
Titles open their catalog pages; version links open the Lean source directly.
The following papers present our team's solutions to previously open research questions.
| Formalization | Source | Contributors | Resources |
|---|---|---|---|
| A Counterexample to Global Convergence of Classical DFP Under the Standard Strong Wolfe Conditions Benqi Liu, Zichen Wang, Zaiwen Wen, Liwei Zhang, and Yaxiang Yuan |
v4.32.0 |
Zichen Wang | arXiv |
| A Fixed-Penalty Linearized Augmented Lagrangian Method with Classical Multiplier Updates Benqi Liu, Kangkang Deng, Zichen Wang, and Zaiwen Wen |
v4.32.2 |
Zichen Wang, Zaiwen Wen | Docs | Verso | Theorem map |
| The Minimum Q-Order of BFGS with Exact Line Search Is One Benqi Liu, Chenyi Li, and Zaiwen Wen (2026) |
v4.32.2 |
Chenyi Li | Source only (documentation pending) |
| Technical note: a counterexample to the Rockafellar sum conjecture on c₀ Junyu Zhang, Jinbiao Chen, Zichen Wang, Benqi Liu, and Zaiwen Wen (2026) |
v4.32.0 |
Zichen Wang | Source only (documentation pending) |
| Formalization | Source | Contributors | Resources |
|---|---|---|---|
| Smooth Minimization of Non-Smooth Functions Yurii Nesterov (2004) |
v4.26.0v4.30.0 |
Wanli Ma, Zichen Wang, Zaiwen Wen | Docs | Verso |
| On Some Local Rings Mohamad Maassarani (2025) |
v4.26.0v4.30.0 |
Liang Xiao, Haochen Ju, Zichen Wang, Zaiwen Wen | Docs | Verso |
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.Zversions are accepted. - Book and paper code is not merged to
main.mainremains 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.
| Category | Project | Description |
|---|---|---|
| Formalization platform | ReasLab | An online Lean formalization platform for collaborative theorem development and verification. |
| Formalization project | Optlib | A Lean4 library for mathematical optimization, covering convex analysis, optimality conditions, and algorithm convergence. |
| ReasBook | A Lean4 project for textbook and paper formalization, including both theorem proving and computational problems. | |
| Benchmark | AMBER | A Lean4 benchmark for construction and verification in applied mathematics formalization, covering both theorem-proving and computational problems. |
| CAM-Bench | A Lean4 benchmark for formal theorem proving in computational and applied mathematics. | |
| Autoformalization and theorem proving | M2F | A toolkit for converting natural-language mathematical textbooks into formalization-ready Lean projects. |
| SITA | A structure-to-instance autoformalization framework for generating Lean definitions/theorems with verification feedback. | |
| lean-tools-mcp | A Lean MCP server with higher parallel throughput and lower memory usage for heavy imports (especially Mathlib). |
- 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)
- 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)
- 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
- 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.
- 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)
- Chenyi Li, School of Mathematical Sciences, Peking University, China (
lichenyi@stu.pku.edu.cn) - Wanli Ma, Beijing International Center for Mathematical Research, Peking University, China (
wlma@pku.edu.cn) - Zichen Wang, School of Mathematical Sciences, Peking University, China (
zichenwang25@stu.pku.edu.cn) - Ziyu Wang, School of Mathematical Sciences, Peking University, China (
wangziyu-edu@stu.pku.edu.cn) - Zaiwen Wen, Beijing International Center for Mathematical Research, Peking University, China (
wenzw@pku.edu.cn) - 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
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/<project>/, and the output
of git rev-parse HEAD. This repository also provides
CITATION.cff for citation tools and GitHub's citation
interface.
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.