Developed by the MathTensor team, this pioneering system is at the forefront of the AI4Math revolution, designed to bridge the gap between complex mathematical intuition and rigorous, machine-verifiable logic. It represents a major leap forward in AI-driven mathematical discovery, transforming highly complex problems into verifiable Lean 4 proofs.
Conquering Putnam 2025 This repository showcases a landmark achievement: MathTensor has successfully solved and formally verified all problems from the Putnam 2025 competition. Long considered the gold standard for human mathematical ingenuity, the Putnam exam requires profound analytical thinking and creative problem-solving. MathTensor has synthesized complete, flawless, and reproducible formal proofs, all strictly verified by the Lean 4 and Mathlib environment.
The Vision & Future Applications Solving contest-level mathematics is just our proof of concept. At MathTensor, we believe that mastering formal mathematical reasoning is the critical path to advanced artificial general intelligence (AGI). The core engine behind our system is built to scale, with immense potential to accelerate R&D in fields that demand absolute logical certainty—including software verification, complex hardware design, cryptography, and scientific discovery.
Connect With Us We are rapidly scaling our capabilities and exploring the next frontier of AI logic. If you are a visionary investor, industry partner, or researcher interested in the commercial and scientific future of AI-driven formal reasoning, we would love to hear from you. Contact us at: mathtensor2026@gmail.com
Keywords: AI4Math, Automated Theorem Proving, Lean 4, Formal Verification, Putnam 2025
This repository contains MathTensor’s raw, end-to-end Lean 4 formalizations of the Putnam 2025 problems, with the environment pinned to Lean 4.27.0.
| Problem | Source | Time (min) | Lines | Lemmas/theorems |
|---|---|---|---|---|
| 2025 A1 | [source] | 100 | 279 | 17 |
| 2025 A2 | [source] | 26 | 183 | 11 |
| 2025 A3 | [source] | 62 | 306 | 11 |
| 2025 A4 | [source] | 87 | 302 | 12 |
| 2025 A5 | [source] | 1326 | 857 | 51 |
| 2025 A6 | [source] | 91 | 622 | 56 |
| 2025 B1 | [source] | 216 | 439 | 16 |
| 2025 B2 | [source] | 183 | 693 | 17 |
| 2025 B3 | [source] | 50 | 167 | 8 |
| 2025 B4 | [source] | 49 | 467 | 24 |
| 2025 B5 | [source] | 161 | 457 | 17 |
| 2025 B6 | [source] | 242 | 275 | 1 |
Putnam2025/
├── A1/
│ ├── problem.lean # formal statement
│ └── solution.lean # full proof
├── A2/
│ ├── problem.lean
│ └── solution.lean
├── ...
└── B6/
├── problem.lean
└── solution.lean
The original Putnam 2025 problem statements are published by the Mathematical Association of America (MAA). This repository does not claim affiliation with, endorsement by, or sponsorship from the MAA or the William Lowell Putnam Mathematical Competition.
Some Lean formal problem statements in problem.lean are adapted from or compared against MIT-licensed Lean formalizations, including:
-
AxiomMath/Putnam2025
-
project-numina/Numina-Putnam2025
When multiple formalizations were available, we selected the versions that most closely match the intended meaning of the original problem statements.
The corresponding file-level copyright notices are preserved in the Lean file headers, and the full MIT license notices are collected in THIRD_PARTY_LICENSES.md.
The completed proofs in solution.lean were developed by MathTensor.
This repository uses the MIT License. See LICENSE for details.