Mathematical Reasoning and Formal Theorem Proving
Training models to solve mathematics problems and to write machine-checked proofs in systems such as Lean 4.
Tier Grades
Tier A: Frontier AI labs
feasible
DeepSeek trains math and prover models up to 671B parameters.
Tier B: Indonesian AI labs
stretch
Continued pretraining on 120B math tokens (DeepSeekMath) is a stretch; Indonesian work is not in the sources.
Tier C: Institution units such as ITB
stretch
Fine-tuning a released 7B prover is institution-scale; the 120B-token pretraining is a stretch.
Tier D: Organisations such as SEMAI (PoT, PoC, PoV)
not feasible
The sources show no delivery use case for formal proving.
Where this comes from
Tiers: a) frontier AI labs, b) Indonesian AI labs, c) institution units such as ITB, d) organisations such as SEMAI delivering proof of technology, concept and value. Each rationale cites the anchors below.
Anchors
- ComputeDeepSeekMath 7B: continued pretraining on 120B math tokens with GRPO. DeepSeek-Prover-V2: 671B parameters.
- Data120B math tokens selected from Common Crawl (DeepSeekMath, 51.7% on MATH); DeepSeek-Prover-V2 reaches 88.9% on MiniF2F-test and solves 49 of 658 PutnamBench problems.
- Team size (proxy)Proxy only (author count of an exemplar paper, not a headcount): 11 authors on DeepSeekMath; 18 on DeepSeek-Prover-V2.
- Time horizonMonths.
- Shelf-life signalsGRPO (from DeepSeekMath) adopted widely for reasoning RL, Formal proof models scoring on PutnamBench
- Pipeline roleTier A trains math and prover models; Tier C uses released ones in teaching and research; Tier D draws on the resulting reasoning gains in general models.
Where this comes from
Team size is a proxy (author counts of exemplar papers), not a headcount.
Who and What
Links
R&D TopicMathematical Reasoning and Formal Theorem Proving
Models
Absolute ZeroTsinghua University, reasoning
DeepSeekMath 7B InstructDeepSeek, reasoningDeepSeek-Prover-V2 7BDeepSeek, reasoning
Absolute ZeroTsinghua University, reasoningDeepSeekMath 7B InstructDeepSeek, reasoningDeepSeek-Prover-V2 7BDeepSeek, reasoningUse Casesnone recorded
Who Runs Itnone recorded
Papers
- Generative Language Modeling for Automated Theorem ProvingStanislas Polu et al., arXiv preprint, 2020 founding
- Measuring Mathematical Problem Solving With the MATH DatasetDan Hendrycks et al., NeurIPS 2021 (per arXiv comment), 2021 founding
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal DecompositionZ. Z. Ren et al., arXiv preprint, 2025 state of the art
- Seed-Prover: Deep and Broad Reasoning for Automated Theorem ProvingLuoxin Chen et al., arXiv preprint, 2025 state of the art
- A Survey on Deep Learning for Theorem ProvingZhaoyu Li et al., arXiv preprint, 2024 survey
Where this comes from
The papers to read first: where the direction began, its current best, and a survey when one exists.
Sources
- arxiv.org/abs/2402.03300 https://arxiv.org/abs/2402.03300
- arxiv.org/abs/2504.21801 https://arxiv.org/abs/2504.21801
To cite this page: Project AURION, AI Use-Cases Research & Innovation, "Mathematical Reasoning and Formal Theorem Proving", https://aurion.semai.id/topics/mathematical-reasoning-and-formal-theorem-proving/, records of October 2026.