AI-Assisted Mathematics

AI-assisted mathematics is mathematical research in which artificial intelligence helps suggest conjectures, find counterexamples or constructions, or develop or formalize proofs. In a human-led investigation, AI may contribute a step or suggest a direction. When the system produces the mathematical argument itself, the argument is more specifically called AI-generated. A search can be automated even when people select the problems, specify the checks, or review the output.

These methods overlap with experimental mathematics when a model proposes patterns or candidates for further computation. In an example of human-led discovery, Davies et al. (2021) used machine learning to identify a relationship between a geometric quantity called the natural slope and the knot signature of a hyperbolic knot. The observed pattern guided the authors to a bound relating the two quantities, which they proved. In the FunSearch method, researchers supply an initial program and a rule for scoring candidate solutions. The search automatically scores programs proposed by the model and favors higher-scoring programs when choosing examples for the model's next proposals. This loop can evaluate more candidates than would be practical by hand. It yielded improved constructions for the cap set problem (Romera-Paredes et al. 2024).

The check depends on the kind of result. For example, computer algebra can check a candidate antiderivative by differentiation and symbolic simplification on the stated domain (Wolfram 2026). In formal proof search, a model can propose steps for a proof assistant such as Lean. Lean's kernel checks the resulting proof term against the formal statement. To apply that check to the original problem, the formal hypotheses and conclusion must match the intended claim, and the axioms used in the argument must be accounted for (de Moura and Ullrich 2021, Lean, Tsoukalas et al. 2026).

The Formal Conjectures repository provides Lean 4 statements of open and solved mathematical problems, including targets for automated proof search (Formal Conjectures Authors 2025). VibeMathed (2026) catalogs reported mathematical advances involving AI and records the model's contribution, the status of each claim, and how the result was checked. The name echoes "vibe coding," an informal term for developing software by prompting AI to write and revise code with little direct inspection of it (Karpathy 2025).

OpenAI (2026a) attributed to an internal model an argument and a Lean formalization for the zero-free region . The claimed nonvanishing of the Riemann zeta function there would establish the fixed zero-free bound required by the quasi-Riemann hypothesis. (The stronger Riemann hypothesis would place all nontrivial Riemann zeta function zeros on the critical line .)

In October 2026, OpenAI (2026b) released 722 model-generated manuscripts grouped into 372 families of related results. Many came with Lean formalizations, and the manuscripts were at different stages of verification. A family can include consequences and alternative proofs of the same result, so a manuscript count does not measure the number of distinct problems solved. In his Numberphile interview, Tao discussed how generating proofs at this scale changes the work of checking and understanding them (Numberphile 2026). After verifying a proof, reviewers still need to determine whether the theorem was already known and what it adds to existing work. Broad automated search can complement a mathematician's sustained investigation of a small number of problems (Big Think 2026, Tao 2026).