AI for Mathematics historical archive
Discover major milestones chronologically, see what AI and humans contributed, and reach primary evidence in one or two clicks.
Chronicle timeline
The public repository includes an overview, a manuscript map, PDFs and sources, a Lean library and formalization catalogue, ten selected reasoning summaries and release-history commitments.
The paper's methodology section says an Anthropic employee initially asked an internal research model to study a cryptographic question based on average-case Zero-k-Clique.
In the acknowledgements, the authors state that most proofs and mathematical ideas in the paper were found by ChatGPT.
Meta says human mathematicians selected and guided the research, a separate group of mathematicians reviewed the work, each paper marks passages primarily drafted by researchers versus AI, and prior or…
AGMAI says the recommendations were informed by more than 600 responses from the mathematical community.
FrenzyMath reports about 3.2 million lines of Lean and less than USD 30,000 in LLM and compute costs for the project.
The group says it formed after OpenAI approached some future members about creating an external advisory board; in agreement with OpenAI, those mathematicians instead formed an independent group and invited…
The archive occupies a deliberately different position from Mathlib: it accepts independent completed formalization projects that may not fit Mathlib's tightly integrated library scope, while imposing…
FormalFlow organizes long formalization projects around a shared blueprint and nested planning, proving and review loops.
The public project supplies an authorless mathematical paper, a complete Lean 4 formalization against mathlib's Liouville function, pinned toolchain metadata, build and axiom audits, and proof-route checks.
The declaration emerged from discussions among its initial signatories during a week of intense debate over rapidly improving AI systems and high-profile mathematical problem solving.
Magenta uses a statement judge to check whether a generated Lean statement preserves the original informal problem and an error-attribution judge to decide whether a failed attempt should return to…
The researchers explicitly credit Diego Córdoba and Luis Martínez-Zoroa for the underlying forced-blowup research program and describe using LLMs to push that program from rougher forcing toward smooth forcing…
OpenAI says roughly 10,000 concurrent agents worked for about 88 hours on the successful search, followed by additional Lean formalization and verification.
The benchmark covers Markov chains, renewal processes, random walks, martingales, stopping times, queues, Brownian motion, stochastic calculus, weak convergence, Poisson processes and continuous-time Markov…
Claude agents used Anthropic's Prove2Me workflow to build a dependency graph of formal subproblems and expand it into millions of lines of Lean code.
The public PrimeGaps186 repository contains a Lean 4 development for DHL[40,2] and the 186 prime-gap consequence together with a Python/FLINT numerical certificate.
Palomar was created in response to the increasing volume of machine-assisted and machine-generated mathematics and the difficulty of auditing claims scattered across repositories and announcements.
Claude coordinated dozens of subagents, searched literature and numerical evidence, and produced a paper; Anthropic mathematicians reviewed the result and a Lean formalization passed comparator.
OpenAI states that an internal Astra model generated the mathematical arguments, humans prepared manuscripts with the model, and the model formalized each argument into a Lean certificate.
Problems are selected by mathematicians, paired with bespoke computational verifiers where possible, and categorized by the significance of a solution.
The pilot restricted participants to models whose intermediate checkpoints, training protocols and training data were public.
The declaration grew from a September 2025 Lorentz Center meeting of around 60 participants from 10 countries spanning mathematics, computer science, philosophy, history, social science, industry and…
AlphaProof Nexus organized frontier LLM subagents around the Lean compiler and escalated proof search with specialized tools and evolutionary search.
The model found a construction using tools from algebraic number theory; OpenAI released the proof and a companion paper by external mathematicians who checked and contextualized the argument.
SorryDB crawls eligible public Lean repositories, records reproducible repository and toolchain coordinates for unresolved `sorry` statements, and asks proving systems to replace each proof hole in its…
The internal model worked with limited human supervision; researchers sometimes requested retries or clarifications and selected among attempts.
M2F first translates long mathematical documents into dependency-ordered Lean declaration skeletons and repairs project-level structural inconsistencies, then freezes statement signatures and iteratively…
Aletheia couples an advanced Gemini Deep Think model with iterative verification, revision and intensive tool use intended for research settings where literature navigation and long proof chains matter.
The system uses a general-purpose coding-agent loop as the controller for Lean work and extends it with theorem retrieval, informal proving, verification and auxiliary reasoning tools exposed through an…
The paper studies whether expected prediction error for maximum-likelihood estimation improves monotonically as more data are observed.
GPT-5 proposed multiple directions and several key structural ideas; Ryu checked, reformulated and wrote the rigorous final proof with coauthor Uijeong Jang.
The architecture generates and formalizes useful lemmas, searches formal proofs and handles geometry through a specialist component.
The system uses scaffolded data synthesis, verifier-guided iterative repair and model averaging.
The system iteratively refines whole proofs from Lean feedback and uses test-time strategies for deep and broad search.
Unlike AlphaProof and AlphaGeometry 2 in 2024, the 2025 system consumed official problem statements directly and produced natural-language proofs without manual translation into Lean or another domain-specific…
The model worked from official natural-language problem statements without a proof assistant or internet access during the evaluation.
The pipeline extracts definitions and theorem context from Lean files, asks an LLM to propose new formal statements, checks generated statements through Lean and separates harder candidates for subsequent…
Mathesis translates an informal problem into a Lean 4 statement, scores candidate formalizations for syntactic and semantic quality, and uses downstream prover feedback to prefer statements that can support…
MathArena evaluates models on recurring competitions soon after problems are released and records whether a model predates each competition.
The agent maintains populations of candidate programs, uses language models to propose edits and repeatedly scores outputs with executable evaluators.
DeepSeek-V3 first decomposes problems into subgoals; successful subgoal proofs become cold-start reasoning traces for reinforcement learning.
R1-Zero used reinforcement learning without an SFT cold start, while R1 added multi-stage training and released several distilled open models.
The project represents mathematical constants as vertices and formulas as hyperedges, then searches for integer relations that can expand this graph.
The benchmark was developed with more than sixty mathematicians and emphasized problems requiring hours or days of expert work.
The system performs expert iteration over large Lean datasets and uses a critic to prioritize easier problems and guide deeper proof searches.
The benchmark was designed after frontier reasoning models approached saturation on older datasets such as MATH.
LeanAgent repeatedly ingests new Lean repositories, traces theorem and premise data through LeanDojo, updates a dynamic database, progressively retrains premise retrieval and searches for proofs of `sorry`…
The benchmark derives controllable families of grade-school mathematics problems from symbolic templates.
The o1 series was trained to spend more inference-time computation on multi-step reasoning before producing an answer.
The model was specialized for Lean 4 formal mathematics, refined with reinforcement learning from Lean feedback and paired with an intrinsic-reward Monte Carlo tree-search variant to explore diverse proof…
The benchmark draws theorems from real Lean projects and textbooks and includes tooling for extracting new project contexts.
The workshop series was created specifically around AI technologies for mathematical reasoning and discovery.
AlphaProof used reinforcement learning in Lean for formal proof search, while AlphaGeometry 2 handled the geometry problem with a faster neuro-symbolic system.
Initial neural and symbolic provers solved only a handful of benchmark problems, making the collection a high-difficulty target for formal reasoning.
The method generates retrospective thoughts from known tactics and then uses expert iteration on newly discovered verified proofs.
The winning system fine-tuned DeepSeekMath-Base 7B and combined chain-of-thought with Python tool execution, self-consistency and internal validation sets.
An iterative generation-and-filtering pipeline translates natural-language math problems to Lean 4 statements and back.
Natural-language competition problems are translated into Lean statements, filtered, proved and recycled as synthetic training data.
The benchmark was designed to remain difficult for frontier text and multimodal models and includes detailed evaluation methodology.
The project encodes reasoning, reward modeling, formal tasks, data augmentation and code-interpreter behavior in a unified sequence-to-sequence format.
The model continued pretraining on 120B math-related tokens and then used supervised and reinforcement-learning stages for mathematical reasoning.
AlphaGeometry combines a neural language model trained on synthetic theorem/proof data with a symbolic deduction engine.
Google DeepMind paired a pretrained language model with an evaluator and evolutionary program search.
The verifier scores intermediate reasoning steps rather than only final answers and can be used for selection or reinforcement learning.
The project continued pretraining Code Llama on Proof-Pile-2, a mixture of mathematical web text, scientific papers and mathematical code.
At each step the agent proposed a tactic, executed it in the proof assistant, incorporated errors or new goals into the next prompt and maintained a search history for backtracking.
The benchmark combines visual perception with compositional mathematical reasoning. The initial study found a substantial gap between frontier multimodal models and human performance, while the public project…
The system couples a prover and an evolver through a shared skill library. The prover constructs modular proofs from retrieved and newly generated lemmas, while the evolver transforms verified skills to…
The agents learn interactive tool-use trajectories involving computation libraries and symbolic solvers rather than relying on text-only chain-of-thought.
The AMS response developed during the first year of widespread generative-AI use. A Notices article records that the Society had already amended its Ethical Guidelines and Journal Policies in June 2023 to…
The project extracts proof states, tactics and premise information from Lean repositories and exposes a programmatic proof environment.
The system searches directly over assembly instructions using an AlphaZero-style learning and search procedure. DeepMind reported speedups up to 70% for short sequences and about 1.
Rather than rewarding only a final answer, the project collected human judgments on intermediate reasoning steps and trained process reward models from those labels.
Instead of predicting one proof step and searching over continuations, Baldur fine-tuned language models to generate an entire proof in one pass.
The benchmark covers analysis, linear algebra, abstract algebra, topology and other textbook mathematics.
Language models produce a high-level formal sketch whose subgoals are then discharged by an automated prover.
DeepMind represented matrix multiplication as a tensor-decomposition game and trained an AlphaZero-style reinforcement-learning agent to search the enormous space of factorizations.
Google Research continued pretraining a large language model on scientific papers and mathematical web content, then evaluated chain-of-thought-style solutions across mathematics, physics and other…
Researchers used few-shot prompting to ask large language models to translate informal mathematical statements into Isabelle/HOL.
NaturalProver conditions language-model proof generation on mathematical background references such as definitions and theorems, either retrieved automatically or supplied by humans.
The system learns from its own proof searches and uses a hyper-tree search algorithm inspired by Monte Carlo tree search and AlphaZero.
The framework uses theorem-prover hammers for premise selection while leaving other proof decisions to the language model.
The prover alternated proof search with retraining on newly discovered proofs over statements of varied difficulty.
Clauses are encoded as graphs and scored by transformer-based models. Training proceeds incrementally, while hindsight replay turns intermediate states from unsuccessful searches into additional learning…
The project used supervised machine learning to search large mathematical datasets for predictive relationships and attribution methods to expose which variables drove those predictions.
The work paired a human-written math reasoning dataset with a generator-verifier pipeline. A language model generated many candidate solutions, while a separately trained verifier scored those solutions and…
The benchmark translated problems from AIME, AMC, IMO and educational sources into formal languages.
MATH-AI began as a cross-disciplinary workshop asking how mathematical reasoning could illuminate general AI.
The benchmark covered algebra, geometry, number theory, probability and other competition topics and provided full solution derivations.
The system represents proof search as an end-to-end reinforcement-learning problem and introduces backtracking that lets the agent abandon predicted dead ends and resume from promising alternatives.
The method extracts self-supervised objectives from kernel-level proof terms and trains them alongside tactic prediction.
OpenAI researchers Stanislas Polu and Ilya Sutskever trained generative models over formal mathematical text and integrated them into proof search for the Metamath language.
The project combines online tactic learning, proof search and package-aware instrumentation so machine-learning assistance lives inside the proof assistant rather than as a detached benchmark-only experiment.
The benchmark generates synthetic inequality proofs from axioms and varies properties of training and test distributions so researchers can distinguish memorization-like success from different forms of…
IsarStep converts declarative Isar proofs into sequence-to-sequence examples where a proof fragment has an intermediate proposition removed.
Rather than masking only a flat token span, skip-tree training removes a subtree from a structured mathematical expression and trains a model to reconstruct it, encouraging representations that reflect the…
The work treated mathematical discourse as a retrieval problem rather than only an answer-generation problem.
The system learns from existing formal mathematics, generates additional theorem-proof pairs, and feeds the synthetic corpus back into prover training rather than relying only on scarce human-authored proof…
CoqGym extracted proof states, environments, goals, tactics and proof trees from open-source Coq projects and exposed them through a programmatic interaction layer.
HOList instrumented HOL Light so learning systems could interact with proof states and tactics through a machine-learning environment.
The original release provided millions of generated question-answer pairs per module and evaluated contemporary sequence-to-sequence neural architectures on both ordinary test splits and extrapolation settings.
GamePad instruments Coq so proof states, proof steps, mid-level and kernel-level terms and proof trees can be represented as Python data structures.
The system repeatedly performs proof-search simulations, turns successful and failed attempts into learning signals, and retrains guidance used in subsequent searches.
The authors constructed a large aligned corpus by informalizing Mizar statements into LaTeX-like mathematical text and trained sequence-to-sequence translation models to reconstruct the formal language.
Mathlib organized community-authored Lean definitions, theorems, proofs and tactics into a common mathematical library spanning algebra, analysis, topology, number theory and other areas.
TacticToe records tactic-level proof information from HOL4, learns which proof actions are promising in a new goal state, and searches over complete tactic sequences directly in higher-order logic rather than…
HolStep extracts intermediate statements and conjectures from HOL Light proofs, canonicalizes their textual representation and pairs useful proof steps with negative examples.
The system learns from clause-level traces of successful automated proofs and ranks generated clauses during saturation-style proof search.
The system learns how ambiguous mathematical notation is parsed from aligned corpora and then uses formal semantic constraints to reject syntactically plausible but mathematically ill-typed or unsupported…
Holophrasm parses Metamath statements into tree structures, learns neural models for proof-step generation and proof-state evaluation, and combines them with search over candidate proof trees.
DeepMath encodes conjectures and candidate premises with recurrent and convolutional neural architectures and learns whether a premise is useful for a target theorem.
AITP 2016 explicitly positioned itself as a forum for combining AI and reasoning methods over large mathematical and scientific corpora.
The project focused on large and complex theories, learning from reasoning traces, feedback loops between deduction and learning, and knowledge accumulation across multiple mathematical representation styles.
Lean combined a small proof-checking kernel, an expressive dependent type theory, interactive proof development and extensible automation in one open platform intended for formalized mathematics as well as…
The completed development formalized both the mathematical text and the large computational components needed for the Kepler-conjecture proof.
The system scaled fast learned relevance methods over roughly 150,000 MML formulas and deployed them within the MizAR online reasoning service.
Users could upload HOL Light developments and ask the service to attack new conjectures using learned relevance models, parallel ATP combinations and decision procedures.
The project formalized the theorem together with a substantial mathematical library spanning group theory, linear algebra, Galois theory and real/complex algebraic numbers.
Sledgehammer selects relevant Isabelle facts, translates proof obligations to external ATPs and uses the returned information to help construct proof-assistant-checked proofs.
The challenge supplied common Mizar-derived problems, public rules and a total resource budget intended to make learning, premise selection and other large-theory reasoning strategies directly comparable.
The system repeatedly trains relevance models from existing proofs, invokes automated provers on selected premises and incorporates newly found proofs into subsequent learning rounds.
The formal development encoded the combinatorial argument and computational case checking inside Coq so that correctness reduced to the proof assistant's general verification mechanisms rather than…
The project aimed to formalize both the written mathematical argument and the computer calculations underlying Hales's proof, eventually using HOL Light and Isabelle.
HR searches a space of mathematical concepts, evaluates their interest and uses generated concepts to drive further examples, classifications and conjectures.
The automated search produced a compact equational derivation in a problem that had resisted prior human and machine efforts for decades.
Systems were evaluated in a shared computational environment on standardized theorem-proving problems, making performance comparisons more reproducible and visible.
QED was a field-building vision rather than a single software release, calling for broad cooperation around shared formal mathematical knowledge.
TPTP collected ATP test problems into standardized formats with domain classification and release/version discipline so theorem provers could be tested on comparable inputs.
Metamath separates a very small verifier from explicit proof objects, allowing a large body of formal mathematics to be checked with a minimal trusted mechanism.
Isabelle used higher-order unification and a generic meta-level architecture to encode and reason within several object logics, with tactics and tacticals providing automation.
HOL combined a small trusted logical basis, ML programming and tactics/tacticals for goal-directed interactive proof in higher-order logic.
Nuprl combined constructive type theory, refinement-style proof development, tactics and computational interpretation of proofs.
Graffiti evaluated candidate relations between graph invariants, retained statements without known counterexamples and used heuristics to suppress trivial or redundant conjectures.
The system provided machine checking for proofs in the Calculus of Constructions and evolved through successive implementations into Coq and later Rocq.
Edinburgh LCF avoided retaining complete proof objects by exposing theorem values through a restricted abstract interface whose constructors corresponded to axioms and inference rules.
AM maintained an agenda of potentially interesting mathematical tasks and used general heuristics to decide which concepts, examples and conjectures to explore next.
The method algebraizes elementary geometry: geometric configurations are encoded as polynomial equations and theorem proving is reduced to symbolic polynomial reasoning.
Mizar developed a formal mathematical language, checker and library model aimed at building a cumulative body of computer-verifiable mathematics.
PLTP targeted properties of recursively defined programs that resolution-based first-order provers handled poorly, using domain-specific proof procedures centered on simplification and induction.
Stanford LCF let users state proof goals, decompose them into subgoals and apply simplification and inference commands while the machine checked the resulting formal derivations.
MACSYMA integrated rational functions, algebraic simplification, calculus and related symbolic operations within an interactive extensible system.
Automath represented definitions, propositions and proofs in a highly explicit typed formal language so a computer could verify the correctness of derivations.
The method combines substitution through unification with a single resolution inference scheme, replacing less efficient alternating procedures used in earlier machine theorem proving.
SAINT represented integration as a search problem, using rules of thumb to choose transformations and substitutions that reduced an integral toward solvable forms.
The system combined symbolic deduction with geometric information to prune implausible proof paths, demonstrating an early form of domain-informed heuristic reasoning.
The system encoded logical expressions and searched a space of permissible transformations, prioritizing promising branches with heuristics rather than exhaustive enumeration.
The proposal did not establish AI4Math as a separate field. It established the broader AI research frame within which mathematical reasoning became one of the earliest domains for testing machine intelligence.
The current search, event type, or significance conditions return no events. Adjust a condition or restore the full timeline.
Restore full timeline