AI Is Not Doing Mathematics. It Is Automating Search.
From Python and Mathematica to AlphaProof and AlphaEvolve, the machinery is still representation, search, iteration and verification. The real revolution is scale, not a new form of mathematics.
Keywords: artificial intelligence, mathematics, computational mathematics, numerical methods, symbolic computation, automated theorem proving, large language models, mathematical reasoning, AlphaProof, AlphaGeometry, AlphaEvolve, FunSearch, Lean, verification, scientific discovery
Abstract
Claims that artificial intelligence is beginning to “do mathematics” often confuse three different things: producing a mathematical answer, discovering a previously unknown result, and introducing a new method by which mathematical truth is established. They are not equivalent. Modern AI systems have become extraordinarily effective at proposing candidate solutions, searching large spaces of possible proofs or algorithms, selecting promising paths and coupling those proposals to computational verification. Yet these operations belong to a much older tradition of computational mathematics. Numerical analysis, computer algebra, optimisation, automated theorem proving and scientific computing have for decades proceeded by representing a problem formally, applying admissible transformations, generating or refining candidate solutions and testing those candidates against explicit criteria. Python, MATLAB, Maple and Mathematica differ enormously in implementation, but the underlying epistemic structure is familiar. Recent systems such as FunSearch, AlphaGeometry, AlphaProof and AlphaEvolve increase the scale and sophistication of candidate generation and search. Some have even discovered genuinely new mathematical constructions and algorithms. That is important. It does not, however, mean that a machine has invented a new mathematics. The strongest AI systems work precisely because their uncertain generative component is constrained by something considerably less fashionable and considerably more reliable: conventional computation, formal logic, objective functions and verification. AI is changing the economics of mathematical exploration. It is not changing what makes mathematics true.
The strange claim that machines have suddenly learned mathematics
There is a peculiar way in which artificial intelligence is discussed at the moment. A model answers an Olympiad problem and we are told that it can reason. A program discovers an improved construction and we are told that artificial intelligence has become a mathematician. An agent searches through possible algorithms and finds one that beats a known result, and suddenly we are invited to imagine a fundamentally new form of mathematical intelligence emerging from silicon.
Much of this language tells us more about contemporary marketing than it does about mathematics.
Computers have been solving mathematical problems for decades. They have been solving them numerically, symbolically, combinatorially and deductively. Anyone who has spent serious time doing computational mathematics already knows the basic pattern. Define the problem. Represent it in a form that the machine can manipulate. Apply an algorithm. Generate an approximation, transformation, candidate or proof state. Evaluate it. Continue if necessary. Check the answer.
Sometimes that means Python. Sometimes it means MATLAB. Sometimes Mathematica or Maple. Sometimes it means C or Fortran wrapped around a numerical library. Sometimes it means a SAT solver, mixed-integer optimiser, Gröbner-basis package, computer algebra system or theorem prover. Today it may mean placing a large language model at the front of the pipeline and allowing it to suggest promising things to try.
The interfaces change dramatically. The computational resources change by orders of magnitude. The search heuristics improve. What has not suddenly appeared is a new criterion of mathematical truth.
That distinction matters because “solving mathematics” is being used to describe several different activities that should not be conflated.
A machine can calculate an answer. It can search for an answer. It can verify an answer. It can find a proof within a formal system. It can search a space so extensively that it encounters a construction nobody had previously recorded. It can even produce a genuinely novel algorithm. Each of those achievements can be important. None requires us to conclude that mathematics itself has acquired a new epistemology.
The difference becomes obvious if we look at what computational mathematicians were already doing.
Suppose I want a numerical solution to f(x) = 0. One familiar approach is Newton’s method,
xₙ₊₁ = xₙ − f(xₙ)/f′(xₙ).
I choose an initial value. The machine evaluates the function and its derivative. It produces another value. It measures whether I am sufficiently close to the required condition. If not, it repeats the calculation. Other root-finding methods alter the details. Optimisation procedures do something similar with objective functions, gradients, Hessians, trust regions, line searches or populations of candidate solutions. Numerical linear algebra introduces an enormous range of direct and iterative methods. None of this is intellectually trivial. Questions of convergence, conditioning, numerical stability and error control are deep mathematical questions in their own right (Higham, 2002; Nocedal & Wright, 2006; Trefethen & Bau, 1997).
“Loop and check” is therefore a useful intuition, but it should not be mistaken for a literal description of every computational method. Gaussian elimination is not simply blind trial and error. Symbolic factorisation need not search randomly through possible answers. A proof kernel can deterministically check a proof term. Computer algebra contains exact algorithms whose mathematical structure matters enormously.
The deeper commonality is this: a problem is encoded in a representation; the machine is given permissible operations over that representation; computation transforms one state into another; and some explicit condition determines whether the result is valid, useful, converged, optimal or complete.
That was computational mathematics before the current AI boom. It remains computational mathematics afterwards.
Computer algebra makes the continuity even clearer. Systems such as Mathematica and Maple do not merely operate giant calculators. They manipulate formal mathematical objects according to algorithms. Polynomial factorisation, symbolic integration, simplification, equation solving and algebraic elimination all depend upon substantial bodies of mathematical theory. Gröbner bases, for example, turned parts of commutative algebra and algebraic geometry into algorithmically tractable computational procedures. Buchberger introduced the foundational algorithm in the 1960s, and variants of Gröbner-basis computation are now implemented throughout major computer algebra systems (Buchberger, 2023; Herzog & Hibi, 2018).
Nobody normally says that Maple becomes a mathematician when it computes a Gröbner basis that would take a human an absurd amount of time to derive manually. Nor do we claim MATLAB has acquired mathematical intuition because an optimisation routine finds parameters that minimise an objective function.
We describe the software as performing computation.
The peculiar thing about contemporary AI is that changing the interface from a command line or explicitly programmed algorithm to natural-language interaction has encouraged people to change the ontology of what the machine is doing.
The output looks like ours, therefore the process is assumed to be like ours.
That conclusion does not follow.
The mathematics is in the representation and the test
Large language models complicate the picture because they are not conventional symbolic systems. An LLM does not ordinarily calculate an expression by internally executing precisely the algorithm a numerical-analysis textbook would prescribe. It generates tokens according to a learned statistical model. Mathematical patterns, expressions, proof forms and common transformations are represented in its learned parameters, allowing it to produce remarkably convincing mathematical text.
That ability is useful. It is also the source of confusion.
Early work on mathematical language models demonstrated both phenomena at once. The MATH benchmark was created precisely because mathematical problem solving remained difficult for large neural models. Its problems included detailed worked solutions, allowing researchers to test whether models could produce multi-stage derivations rather than merely guess short answers (Hendrycks et al., 2021). Minerva subsequently showed that a language model trained heavily on technical material could produce substantial improvements on quantitative reasoning benchmarks (Lewkowycz et al., 2022). Chain-of-thought prompting likewise demonstrated that eliciting intermediate steps could markedly improve performance on arithmetic and symbolic reasoning problems (Wei et al., 2022).
These developments are interesting. They do not eliminate the basic reliability problem.
A fluent mathematical derivation is not necessarily a proof.
Mathematics has an unusually unforgiving relationship with plausibility. A historian can make an argument whose evidence is incomplete yet still illuminating. An economist can construct a model whose assumptions are debatable but whose implications remain interesting. Mathematics has areas in which judgement, interpretation and choice of abstraction matter enormously, but once a theorem has been stated within a formal framework, the proof either establishes the result or it does not.
A nearly valid proof is an invalid proof.
An elegant hallucination is still a hallucination.
This is why the most impressive contemporary AI mathematics systems increasingly place something other than an LLM in the position of final authority.
The language model proposes.
Something else checks.
That architecture is revealing.
FunSearch provides a particularly clean example. Romera-Paredes et al. (2024) combined a pretrained language model with an evaluator in an evolutionary search procedure. The model generated programs. Those programs were executed. Their outputs were scored by an explicit evaluation function. Invalid or poor candidates could be discarded while promising candidates were fed back into further rounds of generation.
Generate. Evaluate. Retain. Mutate. Repeat.
There is nothing embarrassing about that procedure. Quite the contrary. It is powerful precisely because it refuses to trust the language model.
FunSearch famously produced improved constructions for the cap-set problem and new heuristics for online bin packing (Romera-Paredes et al., 2024). These were meaningful results. In the cap-set case, the system went beyond previously known constructions. It would therefore be wrong to dismiss the output merely as memorisation.
But examine where reliability entered the architecture. It was not supplied by linguistic confidence. The system was constructed around problems for which proposed solutions could be objectively evaluated. The LLM enlarged and enriched the space of candidate programs. The evaluator determined whether those candidates actually worked.
This distinction between generating and knowing is central.
A generative system can be extraordinarily valuable if candidate generation is the bottleneck. Many mathematical and computational problems have highly asymmetric difficulty. Finding a good object may be extraordinarily difficult while checking that object is comparatively cheap. Computer science has formalised versions of precisely this asymmetry. The conceptual difference between discovering and verifying is much older than generative AI.
If I give a program the power to generate a million candidate constructions and a deterministic evaluator capable of rejecting 999,999 of them, the surviving construction can be genuinely new. The novelty of the surviving object does not imply that the program has invented a new criterion for mathematical knowledge.
It means search has become cheaper.
This is where I think much of the public discussion goes wrong. AI’s contribution to mathematics may be substantial, but the important change is largely economic.
The cost of producing candidate ideas is falling.
The cost of exploring combinatorial spaces is falling.
The cost of translating between informal and formal representations is falling.
The number of paths that can be examined before a researcher gives up is rising.
The ability to allocate computation towards promising branches is improving.
That can change mathematics enormously without changing the foundations of mathematical validity at all.
Proof systems make the mechanism impossible to hide
Automated theorem proving is especially useful because it strips away the rhetoric.
The idea is not new. Newell, Shaw and Simon’s Logic Theorist dates to the 1950s and is generally regarded as the first major automated theorem-proving system. Automated deduction developed through resolution methods, unification, proof search and eventually sophisticated interactive theorem provers and proof assistants. Long before ChatGPT existed, computers were already finding or checking logical derivations.
Modern proof assistants such as Lean provide an extraordinarily powerful environment for formal mathematics. In Lean, mathematical statements are represented formally, and proof terms can be checked by a small trusted kernel. Mathlib has developed into an extensive community-maintained body of formalised mathematics (de Moura et al., 2015; The mathlib Community, 2020).
This separation between proof discovery and proof checking is crucial.
A complicated automation system may suggest tactics. A human may provide them. An LLM may provide them. A reinforcement-learning system may search for them. None receives the final vote merely because it sounds convincing.
The proof kernel does.
That is exactly why AlphaProof is interesting.
AlphaProof did not solve the reliability problem by teaching an LLM to speak more confidently about mathematics. It placed learned mathematical search inside a formal environment where candidate steps could be executed and proofs could ultimately be verified. Hubert et al. (2026) describe AlphaProof as a reinforcement-learning agent operating within Lean. Its neural component proposes promising tactics and estimates proof difficulty. Tree search explores possible proof paths. Lean executes the tactics and maintains the formal proof state. The kernel ultimately determines whether the resulting proof term is valid.
This is enormously sophisticated computation.
It is also recognisable computation.
The system represents a theorem as a state. At any point there are admissible actions. An action changes the state. Search explores sequences of actions. A value mechanism attempts to allocate computational effort towards promising branches. Successful terminal states correspond to verified proofs.
That is far more powerful than repeatedly throwing random equations at a wall, but conceptually we have not left algorithmic search.
Indeed, the AlphaProof paper is unusually instructive because its scale makes the underlying procedure so visible. The system was initially trained on code, mathematical material and human-written formal proofs. A much larger collection of formal problems was then created using auto-formalisation. Reinforcement learning allowed the system to accumulate experience from successful and unsuccessful proof attempts. For particularly difficult problems, additional problem variants could be generated and used for target-specific learning. Tree-search budgets could also be increased so that more potential proof paths were examined (Hubert et al., 2026).
This is not magic.
It is search engineering of an extremely advanced kind.
The machine has a formal state.
It proposes a tactic.
The environment applies it.
The resulting state is observed.
The search continues.
If a complete proof is constructed, the proof is checked.
The important innovation is the quality with which the system learns which branches are worth exploring.
Human mathematicians do this too, of course. A good mathematician does not attempt every possible algebraic manipulation. Expertise lies partly in knowing which transformations are promising, which analogy may matter, which lemma is likely to unlock the problem, which representation is productive and which line of attack should be abandoned.
Machine learning can provide a heuristic approximation to precisely that selection problem.
That can produce an enormous acceleration.
It still leaves us with an important distinction between heuristic intelligence and mathematical validity. The neural network may tell the system where to look. It is the formal machinery that determines whether what it found is a proof.
AlphaGeometry follows much the same philosophical architecture. Trinh et al. (2024) constructed a neuro-symbolic system in which a learned model guides a symbolic deduction engine. The neural component helps propose useful auxiliary constructions. The symbolic component performs reliable deduction. AlphaGeometry solved 25 of a set of 30 Olympiad geometry problems used in its evaluation, a substantial advance over the previous system examined by the authors.
Again the important word is hybrid.
When a mathematical result absolutely must be right, the most successful systems have repeatedly rediscovered the usefulness of deterministic machinery.
The fashionable component explores.
The unfashionable component checks.
But what about genuinely new discoveries?
This is where the argument requires care.
It would be easy to make the opposite mistake and claim that because AI systems employ search, they therefore cannot produce anything novel.
That is false.
Search can discover things nobody has previously discovered.
An algorithm does not cease to be novel because a computer found it.
A mathematical construction does not become old because it was reached through evolutionary search.
An unknown proof does not become a known proof merely because the theorem and axioms already existed.
We therefore need to separate novelty of method, novelty of path and novelty of result.
FunSearch produced constructions that improved upon previously known results. AlphaTensor used reinforcement learning to discover matrix-multiplication algorithms and found algorithms that improved known computational procedures in specific settings (Fawzi et al., 2022). AlphaEvolve extended the architecture further, using language models to generate and modify programs while automated evaluators tested them and an evolutionary process retained promising variants (Novikov et al., 2025).
AlphaEvolve is perhaps the strongest objection to the simplistic statement that AI “only repeats what it has seen”.
It does not.
According to Novikov et al. (2025), AlphaEvolve discovered algorithms and constructions that exceeded previously known results across several computational and mathematical problems. One widely discussed result was a method for multiplying 4 × 4 complex-valued matrices with 48 scalar multiplications, improving upon the previously known bound for that setting. The system has also been used across optimisation and mathematical search problems where executable candidate solutions can be automatically evaluated.
That is novelty in a perfectly respectable sense.
If nobody knew construction C yesterday, and a computational system produces C today, and C is subsequently verified, then new mathematical knowledge has been produced.
Attempting to define that away because a computer performed the search would be silly.
But the result does not support the larger claim sometimes smuggled into it.
AlphaEvolve does not establish mathematical propositions because Gemini has developed a mysterious machine equivalent of intuition. Its design explicitly combines generative models with evaluators and evolutionary selection. Candidate code is generated. It is executed. It is scored. Better candidates are retained and used to produce further candidates. Search moves through the space of possible programs under the pressure supplied by an objective evaluator (Novikov et al., 2025).
The pattern is almost embarrassingly familiar.
Proposal → evaluation → selection → variation → proposal.
A computational mathematician could recognise the family resemblance immediately.
The difference is that the proposal mechanism has become enormously richer.
Traditional optimisation requires us to specify variables and perhaps a parameterisation before searching. Genetic programming searches over program structures but historically suffered severe problems of scale and representation. Brute-force enumeration explodes combinatorially. Hand-designed heuristics restrict the search according to what the programmer already believes is plausible.
An LLM offers a remarkable new proposal distribution.
Because it has absorbed vast quantities of mathematical text and code, it can generate structured candidates that are not random strings. It can recombine known programming patterns. It can propose modifications whose syntax and semantics are often sufficiently coherent to execute. It can respond to feedback and alter previous candidates. Combined with parallel evaluation and evolutionary retention, this provides a powerful way to explore spaces that were previously too expensive to search effectively.
That is a major technological advance.
But notice where the advance sits.
It sits in search.
It sits in prioritisation.
It sits in candidate generation.
It sits in the cost of exploration.
It does not abolish the evaluator.
In fact, the strongest results make the evaluator more important.
The more prolific the generator becomes, the more indispensable reliable rejection becomes.
A system capable of producing ten possible answers poses one verification problem. A system capable of generating ten million plausible answers poses a much larger one. Generative abundance does not eliminate epistemology. It creates a filtering problem.
This is why I would describe contemporary mathematical AI not as a replacement for computational mathematics but as another layer in it.
Python did not replace numerical analysis. It made implementing numerical analysis easier.
MATLAB did not invent linear algebra. It made sophisticated linear-algebra computation accessible.
Mathematica did not replace symbolic mathematics. It automated enormous quantities of symbolic manipulation.
Lean did not redefine proof. It created a machine-checkable environment in which formal proof could be constructed and verified.
An LLM-guided mathematical agent does not abolish those layers. It sits above them, suggesting what might be worth doing next.
And this is exactly where it can be useful.
Mathematics is not the answer. Mathematics is why the answer follows.
Part of the confusion comes from treating mathematical problem solving as answer production.
Ask a school arithmetic question and that seems reasonable. If I ask for 731 × 219, the answer matters. How it was obtained may be uninteresting.
At higher levels of mathematics, however, the answer is frequently the least important part.
What matters is why the result follows.
A conjectured theorem is not a theorem because somebody guessed the right conclusion.
A numerical coincidence is not an identity.
A million successful tests do not normally constitute a proof of a universal proposition.
A construction that appears optimal for all cases we examined has not necessarily been proved globally optimal.
Mathematics is therefore particularly resistant to the contemporary habit of evaluating artificial intelligence by whether its output resembles a successful human output.
The problem is not resemblance.
The problem is entailment.
This is the importance of formal verification. A system such as Lean allows the relevant definitions, assumptions and steps to be encoded so that a machine can verify whether the proof term follows from the specified formal system. The mathlib project has accumulated a large formal library precisely because formal mathematics depends on definitions and previously established lemmas being represented with sufficient precision to support subsequent proofs (The mathlib Community, 2020).
A language model can assist enormously with that process.
It can suggest a lemma.
It can translate prose into formal syntax.
It can propose tactics.
It can explain an error.
It can search documentation.
It can construct candidate proofs.
It can perhaps identify patterns that a human has missed.
But if I want certainty that a formal theorem has been established, I do not ask whether the language model feels confident.
I check the proof.
That is not a minor engineering detail. It is the entire epistemic distinction.
This also explains why benchmark performance can mislead. When a model is tested against a database of questions whose answers are already known, correctness can be measured by comparing the model’s answer with the reference answer. That tells us something useful about the model. It does not recreate the situation faced by a mathematician working at a genuine research frontier.
At the frontier there may be no answer key.
If the model says that a proposition is true, the interesting question is not whether its prose is persuasive. We need either a valid proof or some other rigorous means of verification.
This creates a paradox of sorts for the most extravagant claims about AI mathematics.
The less we trust conventional mathematical verification, the less reason we have to believe the AI result.
The more important an AI-generated mathematical result becomes, the more strongly we demand the traditional machinery of mathematical checking.
AI therefore does not escape mathematics.
It becomes useful by submitting to it.
The real revolution is the economics of search
None of this makes AI unimportant. It suggests a different account of why it may be extremely important.
The scarcity being attacked is not mathematical truth.
It is human attention.
Consider the daily work of computational research. Researchers spend extraordinary amounts of time translating between mathematical notation and code, testing parameterisations, reading documentation, constructing experiments, checking boundary cases, finding numerical instabilities, debugging implementations, reformulating optimisation problems, generating counterexamples, manipulating symbolic expressions and discarding approaches that do not work.
Much of mathematical research consists not of a continuous sequence of brilliant insights but of enormous amounts of disciplined elimination.
Try this.
No.
Try that.
Fails in dimension six.
Alter the assumption.
Check the limiting case.
Run it again.
That candidate violates the constraint.
This transformation explodes numerically.
That proof path produces an impossible subgoal.
This bound is weaker than the existing one.
Go back.
Try something else.
A good mathematical researcher is not simply a generator of inspiration. A good researcher is also extraordinarily effective at managing search.
This is where AI changes the production function.
Imagine a researcher who can seriously explore five candidate approaches in a day. Now give that researcher machinery capable of generating, implementing and rejecting five thousand candidate variants while preserving the best few for human inspection.
The mathematics has not changed.
The feasible search frontier has.
That distinction is similar to what happened with earlier computational tools.
Before modern numerical computing, some models were effectively unusable because evaluating them was prohibitively expensive. Faster computation did not alter the equations. It altered which equations could be investigated economically.
Computer algebra made symbolic manipulations feasible at scales where hand calculation became ridiculous.
SAT and SMT solvers transformed problems that could be represented as formal constraint systems.
Proof assistants made it possible to verify enormous formal arguments at a level of granularity no human referee could realistically reproduce manually.
AI can push this process another stage forward by reducing the cost of deciding what to try.
That is not a small achievement. It may eventually be one of the largest changes in the practical organisation of mathematical research.
But it is a productivity story before it is a metaphysical one.
The distinction also explains why human involvement remains important.
A search procedure only operates over the space it has been given.
Someone still has to decide what the problem is.
Someone has to decide which representations are meaningful.
Someone has to determine what counts as success.
Someone has to notice when the objective function rewards a mathematically irrelevant artefact.
Someone has to ask whether a computationally superior construction teaches us anything.
Someone has to generalise an observed pattern into a theorem worth proving.
Someone has to recognise when the original question was badly posed.
The evaluator is never philosophically neutral merely because it is executable.
If I tell an optimiser to minimise the wrong function, it may perform magnificently and solve the wrong problem.
If I construct a benchmark with a hidden shortcut, a model may dominate the benchmark without acquiring the capability I thought I was measuring.
If I ask an evolutionary system to maximise a quantity, it may find an obscure boundary condition that satisfies my code while defeating my intention.
Computational researchers have known this forever.
Garbage in, garbage out remains undefeated by artificial intelligence.
Search is not the insult people think it is
There is another mistake worth avoiding.
People sometimes respond to this argument by saying that human mathematics is “just search” as well.
At one level, that observation has force.
Humans certainly explore. We try possible substitutions. We recall similar theorems. We test examples. We move between representations. We abandon failed approaches. We sometimes discover a proof only after days or years of searching.
Calling something search therefore does not automatically make it unintelligent.
The relevant question is what sort of search is occurring and how the search space is being structured.
Blind enumeration is one extreme. Human mathematical research is at another. Expertise compresses the space of possibilities. Mathematical taste tells an expert that one formulation is likely to be fertile and another dead. Analogy imports structure from another area. Conceptual invention changes the representation itself, sometimes turning an impossible search into a trivial one.
Machine learning matters because it can increasingly supply sophisticated heuristics of this kind. A neural model trained over enormous amounts of mathematics can assign different probabilities to possible next moves. It need not search uniformly. Reinforcement learning can sharpen those priorities according to feedback. Tree search can allocate more computation to promising branches.
This is why AlphaProof performs better than a theorem prover that simply enumerates Lean tactics arbitrarily.
The learned component contains information about where successful proofs tend to live.
Likewise, an LLM proposing program modifications for AlphaEvolve is much more useful than a generator replacing characters at random. Its training has given it a structured prior over programs that humans are likely to write and modifications that may preserve some useful coherence.
So the claim should not be that AI is “merely brute force”.
Often it is not.
The better formulation is that AI is making search increasingly informed.
This is where parallels with human mathematical practice become genuinely interesting. A student searches badly. An expert searches selectively. A revolutionary mathematician may redefine the representation so that the old search problem disappears.
Whether machine systems can independently perform that final move in a deep and general way remains a considerably harder question than whether they can score well on established mathematical benchmarks.
A machine that learns to navigate an existing formal environment extraordinarily well is impressive.
A machine that helps discover an unknown construction is more impressive.
A machine that autonomously invents a new mathematical language because the existing language obscures an entire class of structures would be more interesting again.
Those are different achievements.
We should not pretend they have already collapsed into one another merely because they are all described with the letters “AI”.
What AI actually adds
What, then, has AI brought to mathematics that Mathematica, Maple, MATLAB and Python did not?
The answer is substantial, but it is more specific than the marketing.
It provides a probabilistic interface between informal human intentions and formal computational operations.
That is extremely useful.
Traditional mathematical software demands that the user already knows a great deal about what operation should be performed. The researcher chooses a solver, formulates an objective, selects an algorithm, provides parameters, writes code or constructs the symbolic expression in the required form.
A language model can move some of that burden upstream.
I can describe what I am trying to achieve.
The model can propose code.
It can recommend transformations.
It can produce a formalisation.
It can suggest proof tactics.
It can create tests.
It can alter an implementation after observing failure.
It can connect tools that previously required substantial manual glue code.
In an agentic system, those capabilities can be placed inside a loop so that the model observes computational feedback and proposes the next operation.
That looks dramatically more autonomous than running scipy.optimize.
Yet, once again, examine the architecture.
The model proposes some Python.
Python runs.
The result is measured.
The model changes the program.
The program runs again.
The result improves or deteriorates.
The loop continues.
This is a new and extraordinarily flexible way to operate the machinery. It is not a replacement for the machinery.
The distinction is obvious whenever the language model gets arithmetic wrong and quietly calls a calculator to correct itself.
Nobody concludes that the calculator has become less important because the model decided when to use it.
The same principle extends upward.
An AI agent may choose a numerical method.
The numerical method still determines the calculation.
It may invoke Mathematica.
The symbolic engine still performs the transformation.
It may construct a Lean proof.
Lean still determines whether the proof term type-checks.
It may generate ten thousand candidate algorithms.
The evaluator still determines which algorithms satisfy the specification.
The AI layer therefore functions increasingly as an orchestration and search layer over older and more rigid forms of computation.
That architecture may prove far more useful than attempting to make language models themselves infallible mathematicians.
It takes advantage of what probabilistic models are good at while delegating exactness to systems designed for exactness.
There is a broader lesson here for artificial intelligence.
Generative models are powerful because possibility is cheap.
Science advances because rejection is hard.
Generating a hypothesis is not the same thing as establishing it. Generating code is not the same thing as demonstrating that it satisfies a specification. Generating a proof-shaped paragraph is not the same thing as proving a theorem.
The future scientific system is therefore unlikely to consist simply of a bigger chatbot.
It will consist of generators embedded within increasingly sophisticated systems of external constraint.
Generate.
Execute.
Measure.
Reject.
Revise.
Formalise.
Verify.
Escalate to a human where the evaluator itself is uncertain.
That architecture is not evidence that conventional computation has become obsolete.
It is evidence of precisely the opposite.
Mathematics after the hype
I do not find any of this disappointing.
I find it more interesting than the claim that a giant language model has somehow awakened and become Ramanujan.
The real development is concrete.
We are acquiring machinery that can explore mathematical possibility spaces at scales humans cannot.
We are acquiring systems capable of translating informal mathematical language into executable and formally checkable objects.
We are acquiring better learned heuristics for theorem search.
We are acquiring program-generating systems that can mutate candidate algorithms and retain improvements automatically.
We are acquiring research assistants that can connect symbolic mathematics, numerical computation, formal proof and ordinary programming in ways that dramatically reduce the friction between an idea and its computational test.
Those are serious advances.
They may produce serious mathematics.
Some already have.
But they become easier to understand when we stop pretending that the machine has created a new category of mathematical truth.
A result does not become true because an AI generated it.
A proof does not become valid because an LLM wrote it.
An algorithm does not become superior because a model calls it superior.
A candidate earns its status because it survives the relevant mathematical test.
For numerical work, that might mean convergence, stability and error bounds.
For optimisation, it may mean satisfying constraints and improving the objective under an appropriate definition of the problem.
For symbolic mathematics, it may mean exact equivalence under valid transformations.
For a constructive computational problem, it may mean executing the candidate and verifying its required properties.
For a formal theorem, it means providing a proof accepted by the formal system.
The machine can help enormously with finding the candidate.
It does not get to redefine the test.
That is why the continuity from MATLAB and Mathematica to AlphaProof and AlphaEvolve matters.
The systems look radically different because the search layer has become generative, learned and increasingly autonomous.
Underneath it, mathematics remains stubbornly mathematics.
There is a representation.
There are rules.
There is a search space or sequence of transformations.
There is an object being sought.
There is a criterion determining whether we have succeeded.
And eventually somebody—or something considerably more deterministic than a language model—has to check.
The novelty of contemporary AI is therefore not that computers have suddenly begun solving mathematics.
They have been doing that for a very long time.
The novelty is that we have developed vastly better machinery for deciding what computations, transformations, candidate programs and proof steps might be worth trying next.
That changes speed.
It changes scale.
It changes cost.
It changes which problems are economically feasible to explore.
It can even change what we discover.
Those changes are large enough. There is no need to manufacture a metaphysics around them.
AI is not replacing mathematics.
It is industrialising mathematical search.
And if we understand that distinction, we can use it much more intelligently.
References
Buchberger, B. (2023). Automated programming, symbolic computation, machine learning: My personal view. Annals of Mathematics and Artificial Intelligence, 91, 569–589.
de Moura, L., Kong, S., Avigad, J., van Doorn, F., & von Raumer, J. (2015). The Lean theorem prover (system description). In A. P. Felty & A. Middeldorp (Eds.), Automated deduction—CADE-25 (pp. 378–388). Springer.
Fawzi, A., Balog, M., Huang, A., Hubert, T., Romera-Paredes, B., Barekatain, M., Novikov, A., Ruiz, F. J. R., Schrittwieser, J., Swirszcz, G., Silver, D., Hassabis, D., & Kohli, P. (2022). Discovering faster matrix multiplication algorithms with reinforcement learning. Nature, 610, 47–53. https://doi.org/10.1038/s41586-022-05172-4
Hendrycks, D., Burns, C., Kadavath, S., Arora, A., Basart, S., Tang, E., Song, D., & Steinhardt, J. (2021). Measuring mathematical problem solving with the MATH dataset. Advances in Neural Information Processing Systems, 34.
Herzog, J., & Hibi, T. (2018). Gröbner bases: Statistics and software systems. Springer.
Higham, N. J. (2002). Accuracy and stability of numerical algorithms (2nd ed.). Society for Industrial and Applied Mathematics.
Hubert, T., Mehta, R., Sartran, L., Horváth, M. Z., Žužić, G., Wieser, E., Huang, A., Schrittwieser, J., Schroecker, Y., Masoom, H., Bertolli, O., Zahavy, T., Mandhane, A., Yung, J., Beloshapka, I., Ibarz, B., Veeriah, V., Yu, L., Nash, O., et al. (2026). Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 651, 607–613. https://doi.org/10.1038/s41586-025-09833-y
Lewkowycz, A., Andreassen, A., Dohan, D., Dyer, E., Michalewski, H., Ramasesh, V., Slone, A., Anil, C., Schlag, I., Gutman-Solo, T., Wu, Y., Neyshabur, B., Gur-Ari, G., & Misra, V. (2022). Solving quantitative reasoning problems with language models. Advances in Neural Information Processing Systems, 35.
Nocedal, J., & Wright, S. J. (2006). Numerical optimization (2nd ed.). Springer.
Novikov, A., Vũ, N., Eisenberger, M., Dupont, E., Huang, P.-S., Wagner, A. Z., Shirobokov, S., Kozlovskii, B., Ruiz, F. J. R., Mehrabian, A., Kumar, M. P., See, A., Chaudhuri, S., Holland, G., Davies, A., Nowozin, S., Kohli, P., & Balog, M. (2025). AlphaEvolve: A coding agent for scientific and algorithmic discovery. arXiv.
Romera-Paredes, B., Barekatain, M., Novikov, A., Balog, M., Kumar, M. P., Dupont, E., Ruiz, F. J. R., Ellenberg, J. S., Wang, P., Fawzi, O., Kohli, P., & Fawzi, A. (2024). Mathematical discoveries from program search with large language models. Nature, 625, 468–475. https://doi.org/10.1038/s41586-023-06924-6
The mathlib Community. (2020). The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (pp. 367–381). Association for Computing Machinery. https://doi.org/10.1145/3372885.3373824
Trefethen, L. N., & Bau, D., III. (1997). Numerical linear algebra. Society for Industrial and Applied Mathematics.
Trinh, T. H., Wu, Y., Le, Q. V., He, H., & Luong, T. (2024). Solving olympiad geometry without human demonstrations. Nature, 625, 476–482. https://doi.org/10.1038/s41586-023-06747-5
Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, E. H., Le, Q. V., & Zhou, D. (2022). Chain-of-thought prompting elicits reasoning in large language models. Advances in Neural Information Processing Systems, 35.