mathtensor/ai4math-putnam2025

This repository, from a team called MathTensor, contains formal mathematical proofs for all twelve problems from the 2025 William Lowell Putnam Mathematical Competition. The Putnam is an annual undergraduate math contest known for being very difficult, and the team claims their AI system produced complete, machine-verified solutions to every problem on the exam. The proofs are written in Lean 4, which is a programming language designed for stating mathematics in a precise, computer-checkable way. Each solution uses Mathlib, a large community library of formalized math that Lean programs can build on. Because the proofs are checked by software rather than only by humans, the claim that each problem is solved can be verified by anyone who downloads the repo and runs Lean on it. The environment is pinned to Lean version 4.27.0. The folder layout is simple. There is one directory per problem, named A1 through A6 and B1 through B6, and each directory holds two files: problem.lean with the formal statement of the problem, and solution.lean with the full proof. A summary table in the README lists how long each proof took to produce, how many lines it has, and how many supporting lemmas or theorems it uses. The hardest problem, A5, runs to 857 lines and took over 1300 minutes. The README also notes that some problem statements were adapted from other Lean formalizations released under the MIT license, with attribution kept in file headers. The repo itself is released under the MIT license, and the authors state they have no affiliation with the Mathematical Association of America.