Search, combine conditions, and compare events

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. OpenAI explicitly warns that some unformalized results may contain issues and says revisions will remain accessible. The release followed consultation with the independent Advisory Group on Mathematics and Artificial Intelligence. AGMAI publicly stated that its advice does not endorse the mathematics or OpenAI's process and characterized the release as the beginning of broader human understanding and community assessment.

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. Claude unexpectedly developed a new algorithm, first for the average-case setting and then for the worst case, during a session producing about 16 million output tokens with no human input. Anthropic shared the result with Alman and Vassilevska Williams, who reconstructed the argument, simplified it, improved constants and exponents, derived additional consequences and wrote the research paper. After the paper was complete, Anthropic used a research model to formalize major deterministic claims in Lean.

In the acknowledgements, the authors state that most proofs and mathematical ideas in the paper were found by ChatGPT. They identify the suspension idea as a notable human contribution and describe their role as understanding the model's proofs, checking and organizing the mathematics and improving the exposition. The paper is currently a very recent preprint; Chronicle has not located a public proof-assistant artifact or independent specialist review sufficient to move the event beyond a paper-released verification state.

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 concurrent work is credited. Muse Spark's role varied by project: it helped test and revise calculations, generated a GAP search program that found a 384-element group counterexample, proposed counterexamples and proof strategies, and generated candidate proofs and technical sections. Meta also acknowledges that several questions were independently resolved by other teams, including one semiabelian-group counterexample reported by the Nilradical AI agent before Meta's publication.

AGMAI says the recommendations were informed by more than 600 responses from the mathematical community. The document distinguishes ordinary papers that a responsible mathematician fully understands from AI outputs that nobody yet understands. In the latter case it proposes technical release norms and a parallel obligation for labs to fund independent, community-led workshops, conferences, expository work and other activities needed to assimilate the mathematics. It also warns that unequal access to frontier systems could create a multi-tier 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 repository separates the Mathlib-only endpoint statements from the proof library and preserves Comparator configuration, verifier revisions, logs and source-provenance records. The announcement also notes that an independent team led by Ziyang Qin, Yuan Liao, Ayush Khaitan and Bennett Chow released another complete Poincaré Lean development earlier the same day; that separate arXiv paper records a full public build and says automated assistance was used for proofs and prose.

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 additional members. Its initial membership consists of François Charles, Camillo De Lellis, Timothy Gowers, Martin Hairer, Nikhil Srivastava, Ulrike Tillmann, Ravi Vakil, Edward Witten and Melanie Matchett Wood. The group's first stated task is to advise OpenAI on coordinating the release of a large number of significant mathematical results that OpenAI reports were produced by an internal model. OpenAI's announcement explicitly cites A Severe Misalignment of AI in Mathematics as part of the context for creating this bridge to the mathematical community.

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 automated maintenance and quality checks. The public repository reports that project imports are still selected by humans, while AI systems participate materially in review, maintenance and optimization. The corpus size changes continuously and is therefore not treated as a frozen historical claim in this Event.

FormalFlow organizes long formalization projects around a shared blueprint and nested planning, proving and review loops. AI agents implement and review proof tasks while humans supervise the project, compare the formal development with the source mathematics and resolve semantic discrepancies. The public MIPStarRE repository preserves Lean sources, the active blueprint, source-paper material and CI-oriented proof-integrity infrastructure.

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. A separate audit repository independently rebuilt the frozen v1.0.0 artifact on Linux, matched the source hashes, repeated the axiom and route audits, and reported no sorry, custom theorem axiom, or native_decide. The public paper and repository do not preserve a detailed model–human derivation trace, so the precise division of intellectual labor remains source-attributed rather than independently reconstructed by the Chronicle.

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. It framed the central concern as a misalignment between benchmark-driven corporate incentives and the mathematical community's emphasis on understanding, communication, attribution, mentorship and durable knowledge. On 14 September, IMPA published the statement on its institutional news surface. On 15 September, the board of the French Mathematical Society cited it in an official position responding to the OpenAI Navier–Stokes announcement and its associated ethical controversy.

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 mathematical re-derivation or local Lean repair. The paper reports that this feedback-guided correction loop outperforms independent resampling on difficult problems.

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 and related fluid equations. The public `fluid_lean` repository contains complete Lean developments for the Euler and Boussinesq theorems, with its documentation attributing the Lean code to Claude under Alpöge's direction.

OpenAI says roughly 10,000 concurrent agents worked for about 88 hours on the successful search, followed by additional Lean formalization and verification. Independent reporting corroborated the publication event while also documenting disputes over attribution, provenance and priority involving contemporaneous work by Tristan Buckmaster and Levent Alpöge. OpenAI now says that, following an investigation, Buckmaster's Codex prompts during the two months before the 8 September release could not have influenced the system in any way, including through training. That direct statement narrows one provenance concern, while separate disputes over attribution, priority and the collaboration process remain part of the public record.

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 processes. Its released dataset distinguishes 114 direct formalizations from 336 abstracted targets that expose assumptions explicitly when the required stochastic-process infrastructure is not available in the fixed Lean/Mathlib environment.

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 repository follows the classical Frey-Serre-Ribet-Wiles-Taylor-Wiles route and exposes the theorem graph, source attribution and reproducible verification procedures.

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. The registered main Lean declarations contain no sorry, and OpenAI reports that Comparator, Nanoda and Lean's kernel accepted the conditional proofs. The formal development nevertheless depends on three explicit project axioms: a rank-three hyper-Kloosterman estimate, a rank-two Kloosterman correlation estimate, and a collection of physical-integral and cap bounds. The first two are attributed to established literature; the numerical input is checked by the companion certificate rather than proved inside Lean. OpenAI's own metadata labels the review self-assessed and states that no independent human semantic review had been completed.

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. Its public statement positions the service as analogous to a preprint or repository layer for formalizations: it provides an immutable, searchable and inspectable record of what was mechanically checked while leaving novelty, relevance and deeper mathematical judgment to the research community.

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. Subsequent reporting documented attribution and training-data provenance concerns around the non-sofic-groups result, including Andreas Thom's unresolved question about whether unpublished mathematical discussions conducted through ChatGPT could have contributed indirectly through model-improvement data.

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. Six teams produced evaluated outputs on six proof problems, and AIMO compared them under the same expert-grading procedure with open-weight and commercial frontier models while publishing the submissions and detailed grading data.

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 government. A smaller working group developed the text over the following months with extensive community feedback. The declaration was archived on Zenodo with a DOI, endorsed by the IMU, later discussed at ICM 2026, and the subject of supportive editorials and reporting in major scientific publications.

AlphaProof Nexus organized frontier LLM subagents around the Lean compiler and escalated proof search with specialized tools and evolutionary search. The project released Lean proofs for successful Erdős, OEIS and research-collaboration cases together with human-readable proof writeups for selected results.

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 original project context. A verifier rebuilds the relevant project and checks proposed replacements, while a nightly database refresh supplies new tasks over time.

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 closes proof holes using verifier feedback. The companion ReasBook repository exposes generated formalizations from textbooks and research papers.

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 authors explicitly separated levels of autonomy and novelty rather than treating all AI-assisted results as equivalent.

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 MCP-oriented interface. Its public repository includes setup instructions, runnable agent tooling and links to the Putnam proof artifacts.

The paper studies whether expected prediction error for maximum-likelihood estimation improves monotonically as more data are observed. It proves forward-KL monotonicity for several Gaussian and Gamma settings and gives a reverse-KL argument for broad exponential families. OpenAI presented the work as a case study of GPT-5.2 Pro contributing directly to previously unsolved mathematical questions.

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 formal language. It completed the task within the 4.5-hour competition limit.

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 training. The paper also reports several non-trivial topology examples as evidence that the pipeline can produce mathematically useful statements rather than only superficial perturbations.

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 machine-checked proofs. Gaokao-Formal provides hundreds of challenging proof problems derived from Chinese college-entrance examinations for evaluating this full pipeline.

MathArena evaluates models on recurring competitions soon after problems are released and records whether a model predates each competition. Its public pipeline supports final-answer parsing as well as proof-based competitions such as USAMO and IMO, where expert graders assess model-generated proofs.

The agent maintains populations of candidate programs, uses language models to propose edits and repeatedly scores outputs with executable evaluators. The accompanying technical report and results repository document mathematical cases where the evolved programs improved known constructions.

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 associated LIReC software provides a public database and numerical relation-identification tools for inspecting and extending the library.

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` theorems. Successful proofs can be added back to the knowledge base for later learning.

The benchmark derives controllable families of grade-school mathematics problems from symbolic templates. This lets evaluators vary numerical values, clause counts and distractors while preserving the underlying reasoning structure, testing whether model success is stable rather than tied to a fixed benchmark instance.

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 paths. DeepSeek released model weights and code for reproducing the proof-search setup.

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. By its third edition, the venue reported hundreds of submissions and accepted papers, a multi-level program committee, paper awards and four challenge tracks covering autoformalization alignment, theoretical-computer-science proving, visual scientific reasoning and end-to-end Lean proof generation.

AlphaProof used reinforcement learning in Lean for formal proof search, while AlphaGeometry 2 handled the geometry problem with a faster neuro-symbolic system. The 2024 workflow required experts to translate problems into formal representations and used up to several days of computation.

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. The language model proposes auxiliary constructions and the symbolic engine checks deductions.

Google DeepMind paired a pretrained language model with an evaluator and evolutionary program search. The resulting system searched over executable programs rather than directly emitting final mathematical answers.

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 architecture showed how a frontier general model could be wrapped in a proof-oriented agent harness without task-specific finetuning.

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 provides dataset access, evaluation code and model-result tooling.

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 increase their generality, reuse and complexity.

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 adopt the COPE position that AI tools cannot be authors and AI use must be disclosed. The July advisory group then broadened the response from immediate journal rules to sustained governance questions for mathematical research and the profession. Its 2024 white papers were explicitly intended as living resources for AMS policy committees and the wider community.

The project extracts proof states, tactics and premise information from Lean repositories and exposes a programmatic proof environment. ReProver retrieves relevant premises before generating tactics, directly addressing the library-scale premise-selection problem.

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.7% for very long sequences, while releasing pseudocode and discovered assembly programs with correctness tests.

Rather than rewarding only a final answer, the project collected human judgments on intermediate reasoning steps and trained process reward models from those labels. PRM800K exposes the annotations, labeling instructions and scored model samples used in the study.

Instead of predicting one proof step and searching over continuations, Baldur fine-tuned language models to generate an entire proof in one pass. A separate repair model then received a failed proof attempt together with proof-assistant error feedback and proposed a corrected proof.

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. Released artifacts include discovered factorizations, benchmarking code and checks of algorithmic properties.

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 quantitative domains. The system operated in natural language rather than a proof assistant.

Researchers used few-shot prompting to ask large language models to translate informal mathematical statements into Isabelle/HOL. The generated formalizations were then used as additional training data for a neural theorem prover, linking informal-language translation with formal proof search in one pipeline.

NaturalProver conditions language-model proof generation on mathematical background references such as definitions and theorems, either retrieved automatically or supplied by humans. The project studied both next-step suggestion and full-proof generation and released the NaturalProofs-Gen data, training and generation code, evaluation tooling and model assets.

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 targets instead of discarding those trajectories.

The project used supervised machine learning to search large mathematical datasets for predictive relationships and attribution methods to expose which variables drove those predictions. Mathematicians then interpreted the signals, reformulated them as mathematical statements, tested counterexamples and supplied conventional mathematical arguments. The Nature article demonstrated the workflow on hyperbolic knots and Kazhdan-Lusztig polynomials, alongside public notebooks and datasets for both case studies.

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 selected the most promising answer.

The benchmark translated problems from AIME, AMC, IMO and educational sources into formal languages. Its goal was not a new mathematical theorem but a reproducible common target on which learned theorem provers could be trained and compared.

MATH-AI began as a cross-disciplinary workshop asking how mathematical reasoning could illuminate general AI. The inaugural program combined invited talks, contributed papers, poster sessions and a discussion panel, while its review process used anonymized submissions. Across later editions the series evolved with the field toward large language models, theorem proving, autoformalization, mathematical discovery and agentic AI while retaining a dedicated mathematical-reasoning identity.

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 resulting proofs are constructed inside HOL4 and therefore remain subject to the proof assistant's kernel checking.

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 work framed theorem proving as sequence generation and showed that learned generation could contribute usable proof artifacts to an established formal library.

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 out-of-distribution theorem-proving generalization.

IsarStep converts declarative Isar proofs into sequence-to-sequence examples where a proof fragment has an intermediate proposition removed. The task tests whether a model can reconstruct a semantically useful bridge between surrounding proof states, and the authors evaluated Transformer-based baselines including a hierarchical architecture designed for long proof context.

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 compositional structure of formal mathematics.

The work treated mathematical discourse as a retrieval problem rather than only an answer-generation problem. Its dataset captures links among conjectures, definitions and supporting propositions in ProofWiki, while accompanying baselines and later graph-based experiments measured how effectively models could recover proof-relevant references.

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 traces.

CoqGym extracted proof states, environments, goals, tactics and proof trees from open-source Coq projects and exposed them through a programmatic interaction layer. ASTactic learned proof-step generation from this corpus and composed tactics from runtime syntax rather than relying only on a predetermined list of complete tactics.

HOList instrumented HOL Light so learning systems could interact with proof states and tactics through a machine-learning environment. The benchmark packaged theorem statements from core, complex and Flyspeck corpora with train, validation and test labels, while DeepHOL supplied a neural prover and reinforcement-learning loop for generating additional successful proof traces.

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. The accompanying open-source generator made it possible to reproduce and extend the task distribution rather than treating the benchmark as a fixed static question list.

GamePad instruments Coq so proof states, proof steps, mid-level and kernel-level terms and proof trees can be represented as Python data structures. A lightweight coqtop wrapper lets learning code send tactics and receive parsed proof states, while released tooling supports extracting data from the Mathematical Components odd-order development.

The system repeatedly performs proof-search simulations, turns successful and failed attempts into learning signals, and retrains guidance used in subsequent searches. The approach was evaluated over a large formal-mathematics problem corpus, emphasizing learned search control rather than theorem-specific handwritten heuristics.

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. The study evaluated multiple neural translation configurations and used case studies to examine which mathematical structures could be recovered correctly.

Mathlib organized community-authored Lean definitions, theorems, proofs and tactics into a common mathematical library spanning algebra, analysis, topology, number theory and other areas. Shared APIs and review practices made formal developments composable rather than isolated project artifacts.

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 translating every problem to first-order logic. The 2017 system used a modified A*-style search with tactic prediction and small-scale hammering; the later expanded implementation developed the search machinery further and remains available in the HOL4 repository.

HolStep extracts intermediate statements and conjectures from HOL Light proofs, canonicalizes their textual representation and pairs useful proof steps with negative examples. The release defines conditioned and unconditioned proof-step classification tasks and provides baseline code so researchers can compare learned representations and relevance models on a common formal-mathematics corpus.

The system learns from clause-level traces of successful automated proofs and ranks generated clauses during saturation-style proof search. Because neural evaluation is slower than hand-engineered heuristics, the authors used hybrid guidance and a two-phase search strategy that lets the learned model improve the search trajectory before faster conventional heuristics finish the proof attempt.

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 interpretations. This creates a hybrid statistical-symbolic pipeline in which learning proposes formal structures and theorem-proving machinery helps validate them.

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. The public release includes model-training and proof-search code, saved proof outputs, and instructions for replaying generated proofs through Metamath's verifier.

DeepMath encodes conjectures and candidate premises with recurrent and convolutional neural architectures and learns whether a premise is useful for a target theorem. The release turned large formal proof corpora into training data for neural relevance models, making representation learning a central component of automated theorem-proving pipelines.

AITP 2016 explicitly positioned itself as a forum for combining AI and reasoning methods over large mathematical and scientific corpora. The inaugural program included focused sessions on AI for ATP/ITP and mathematics, informal and semi-formal mathematical understanding, modern AI methods, and contributed talks. Its official series record documents yearly meetings from 2016 through 2026.

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 verification.

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 theorem-specific external programs.

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. Complete proofs could be used to obtain programs meeting formal specifications, linking theorem proving, formal mathematics and verified programming in a single environment.

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. Users could write higher-level proof procedures in the typed functional language ML, while tactics and tacticals supported reusable backward proof strategies.

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. Wu developed the route from Ritt-style characteristic-set ideas and constructive elimination, enabling mechanical proof procedures and explicit treatment of degenerate cases. Later computer implementations proved non-trivial geometry theorems and helped establish algebraic automated deduction in geometry as a durable research program.

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. It predated the extensible ML metalanguage, abstract theorem type and programmable tactics that characterized Edinburgh LCF.

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.