MKLab - AI AND TECHNOLOGY

Rethinking Mathematical Intuition in the Age of AI

Sat, 12 Sep 2026 02:10:29 +0300

Rethinking Mathematical Intuition in the Age of AI
Michael Friedman & Kati Kish Bar-On —
The Mathematical Intelligencer, 26 August 2026

The article argues that artificial intelligence is beginning to change not merely how quickly mathematics is done, but the role of mathematical intuition itself. Traditionally, intuition has often come before a proof: a mathematician develops a sense of which direction might work, proposes a construction or conjecture, and then tries to prove it. AI systems can reverse this order. They may discover a proof, construction, program, or unexpected connection first, leaving humans to understand afterwards why it works. The authors illustrate this with the recent AI-assisted disproof of Erdős Problem #90, where configurations with at least $n^{1+\delta}$ unit distances were obtained using techniques far removed from the approaches mathematicians had pursued for decades.

Three case studies illustrate different forms of this shift. With AlphaGeometry, the system can propose highly non-obvious auxiliary constructions and formally prove that they work; human mathematicians may then have to reconstruct the geometric motivation afterward—what the authors call retroactive intuition. In knot theory, a neural network analysing roughly $2.7$ million knots identified unexpected relationships among invariants, after which mathematicians interpreted the patterns, formulated conjectures and produced proofs. Here intuition becomes co-constitutive: AI discovers promising patterns while humans judge which ones deserve mathematical attention. With FunSearch, the transformation is even stronger. Instead of directly searching for a mathematical object, the AI searches through Python programs that generate objects; this approach improved the cap-set construction in dimension $8$ from $496$ to $512$ elements, with humans extracting a comprehensible mathematical construction only after inspecting the discovered code.

The authors therefore do not argue that AI will eliminate mathematical intuition. Rather, intuition may be relocated from discovery toward interpretation, explanation and selection. This becomes particularly important in what Terence Tao has called an era of “proof abundance”: machines may eventually generate far more correct proofs than mathematicians can meaningfully study. The scarce resource would then no longer be proofs themselves but “proof digestion”—determining which results matter, understanding why they are true, connecting them to existing mathematics, and turning opaque machine discoveries into concepts humans can reason about. The authors warn that if mathematics becomes satisfied merely with verified statements while abandoning the demand to understand why, something essential about mathematical practice could be lost.

ARTICLE

What the Navier-Stokes Solution Portends

Sat, 12 Sep 2026 01:48:20 +0300

Summary

Steven Heilman argues that the significance of OpenAI’s reported solution of the Navier–Stokes Millennium Prize Problem extends far beyond the mathematics itself. He focuses on the circumstances surrounding the announcement: according to Heilman, OpenAI contacted mathematician Tristan Buckmaster, spent an estimated $20 million in compute over roughly four days, and was partly motivated by a desire to reach the result before competitors such as Anthropic. Heilman acknowledges that the AI system apparently succeeded in resolving an extraordinarily difficult mathematical problem, but stresses that it built on a promising strategy already identified by Buckmaster and Levent Alpöge and ultimately inspired by earlier mathematical work.

The central concern of the article is therefore not whether AI can do advanced mathematics, but what incentives are driving AI laboratories. Heilman argues that corporate competition, publicity, investment and valuation may increasingly take priority over the slower academic processes of developing ideas, assigning credit and nurturing researchers' careers. He connects the Navier–Stokes episode with recent AI-assisted work on prime gaps and invokes Terence Tao's warning that mathematics risks being effectively "strip mined" for headlines. In this view, AI laboratories can deploy enormous computational resources against problems on which mathematicians may have spent years, converting unfinished human research directions into highly visible corporate achievements.

His broader warning concerns the future of intellectual labour. The issue is not simply that AI might replace mathematicians; rather, Heilman fears that researchers could become inputs into a system whose primary objective is corporate advantage. Credit disputes matter because recognition affects academic careers, funding and employment, whereas companies have very different incentives: being first, attracting attention and demonstrating technological superiority. The article therefore portrays the Navier–Stokes episode as an early example of a possible transformation in which the economic power surrounding AI changes who controls mathematical discovery, who receives credit for it, and why difficult problems are pursued in the first place.

Key idea: Heilman is less worried that AI can solve mathematics than that corporations with enormous compute budgets may increasingly determine the direction, timing and ownership of mathematical discovery.

ARTICLE

Use of AI in mathematical research

Sat, 12 Sep 2026 01:32:47 +0300

Use of AI in Mathematical Research: A Guide for Young Mathematicians — Pavel Etingof (MIT, May 2026)

Pavel Etingof argues that mathematicians should neither reject AI nor delegate mathematics to it. His central principle is simple: use AI to know and understand more mathematics, while personally remaining fully abreast of every mathematical step it produces. Any AI-generated proof, computation, or argument that enters one's work must be independently checked, understood in detail, and rewritten in the mathematician’s own way. The reason is both practical and educational: LLMs can produce convincing but subtly false arguments, and the researcher—not the AI—is responsible for errors. More fundamentally, struggling with problems is how mathematicians acquire intuition and research ability; outsourcing that struggle defeats much of the purpose of doing mathematics.

Etingof nevertheless sees AI as an increasingly powerful research instrument. It can help with literature searches, explanations, brainstorming research questions, generating examples and computational data, searching for counterexamples, writing code, LaTeX, and proofreading. For proving new results, however, he urges much greater skepticism: AI is considerably safer when explaining established mathematics than when claiming an original proof. One useful procedure is to have another model attack an AI-generated proof, iterate between critics, and then perform the decisive human verification yourself—but agreement between several models is still not evidence of correctness because models may share the same biases and failure modes. He also highlights formal verification with Lean, where LLMs can increasingly help translate mathematical statements into machine-checkable proofs, provided the human verifies that the formal statement actually represents the intended theorem.

The broader message is that AI should be treated as a powerful but unreliable digital collaborator, not an autonomous mathematician. Etingof recommends using it to increase the amount and depth of mathematics one can explore rather than to reduce one's own mathematical effort. Researchers should verify references, protect confidential material, avoid copying AI-generated prose, acknowledge substantial AI contributions, and remain capable of reproducing and explaining everything without access to the original AI conversation. He also stresses that mathematics is fundamentally communal: even a correct machine-generated proof does not become genuine mathematical understanding until humans interpret it, explain its ideas, connect it to existing knowledge, and make it accessible to the mathematical community.

Key takeaways

AI should amplify mathematical thinking, not replace it.
Treat every novel AI-generated proof as unverified until independently checked.
AI may be especially useful for examples, counterexamples, computation, coding, literature search and Lean formalization.
Etingof's final test is particularly strong: if the AI conversation disappeared, could you still understand, reproduce and take full responsibility for everything in your work?

ARTICLE [PDF]

A Severe Misalignment of AI in Mathematics

Fri, 11 Sep 2026 22:40:30 +0300

The declaration “A Severe Misalignment of AI in Mathematics”, endorsed by many leading mathematicians and Fields Medalists, argues that the rapid improvement of AI systems in solving difficult mathematical problems may conflict with the deeper goals of mathematics. The authors stress that solving a famous problem is traditionally valuable not merely because it produces a correct theorem, but because the process generates new concepts, methods, explanations, and understanding that can be absorbed and developed by the mathematical community. Treating unsolved problems primarily as benchmarks for AI risks reducing mathematics to the mass production of correct answers rather than the cultivation of insight.

The declaration also raises concerns about the speed with which AI-generated results may be announced. Rapid publication can leave insufficient time to clarify arguments, identify genuinely new ideas, connect them properly with previous research, and give appropriate attribution—creating possible problems involving credit and plagiarism. Even when AI produces important ideas, human mathematicians are still needed to interpret, simplify, teach, verify, and integrate those ideas into the broader mathematical body of knowledge. Without this process, the authors fear that the traditional chain through which mathematical understanding is transmitted between generations could weaken.

The authors are not rejecting AI in mathematics. They acknowledge that AI could greatly accelerate genuine mathematical research and understanding. Their central warning is that the technology should be designed and used so that it strengthens the purposes of mathematics rather than merely optimizing for impressive problem-solving results. They view mathematics as an early example of a much broader challenge facing science and creative work: as AI becomes capable of producing the outputs of intellectual labor, society must ensure that it does not lose the understanding, education, creativity, and human development that the work was meant to produce.

ARTICLE

Top mathematicians are outraged by OpenAI’s methods

Fri, 11 Sep 2026 21:58:16 +0300

Quote:
Source: The Economist
This is a summary/commentary on the original article.

The original article is available to subscribers at The Economist.

The article argues that the central danger of AI in mathematics is not simply that machines may solve difficult problems faster than humans, but that they may weaken the process through which mathematics produces understanding. The September 11th open letter signed by 24 Fields Medalists responds to recent AI claims such as OpenAI’s apparent solution of the Navier–Stokes problem. Its authors worry that AI labs are treating major mathematical problems as benchmarks: producing technically correct proofs while offering little intuition, explanation, or conceptual insight. For mathematicians such as Terence Tao and Hugo Duminil-Copin, the intellectual value of mathematics lies partly in the journey—the failed approaches, new ideas, intermediate lemmas and new questions generated while seeking a proof—not merely in reaching the final theorem.

The article is strongest when it distinguishes mathematical knowledge from mathematical understanding. A machine-generated 166-page proof could expand what humanity knows while doing comparatively little to explain why something is true. If this became common, mathematics could divide into results that machines can verify and results humans actually understand. That would be particularly troubling in pure mathematics, where understanding rather than immediate practical application is often the main objective.
However, the argument is somewhat speculative. Historical comparisons with writing, calculators and search engines show that intellectual tools often change rather than destroy human abilities. AI could similarly become a partner that discovers proofs while mathematicians extract concepts, simplify arguments and build new theories from them. The cited research on “cognitive offloading” and correlations between AI use and critical thinking also does not directly demonstrate that AI-assisted professional mathematics causes intellectual decline.
A deeper issue that the article only partly explores is the structure of scientific credit and competition. If well-funded AI laboratories can use unpublished or recently published human research, enormous computing resources and private models to finish problems that individual mathematicians have worked on for years, questions arise about attribution, priority, transparency and access—not merely cognitive decline.

Critical conclusion: the Fields Medalists' warning should therefore not be read as opposition to AI doing mathematics. The more important question is what kind of mathematical culture develops around AI. If success is measured only by the number of famous conjectures solved, mathematics risks becoming a scoreboard for AI laboratories. If AI-generated proofs are instead followed by human explanation, simplification, verification and conceptual development, AI could greatly strengthen mathematics rather than undermine it. The challenge is ensuring that solving the theorem does not become more important than understanding the mathematics.

ARTICLE

OpenAI's apparent maths breakthrough raises profound questions

Fri, 11 Sep 2026 19:24:19 +0300

Quote:
Source: The Economist
This is a summary/commentary on the original article.

The original article is available to subscribers at The Economist.

OpenAI claims AI agents solved the Navier–Stokes Millennium Problem

OpenAI says that a large swarm of AI agents has found a solution to the Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems established by the Clay Mathematics Institute. The problem asks whether solutions to the three-dimensional Navier–Stokes equations can develop a finite-time singularity, where a quantity such as fluid velocity becomes unbounded. According to the account, OpenAI began its experiment on September 1st, 2026, using teams of autonomous agents capable of searching the web, running code and collaborating. After an intermediate breakthrough, around 10,000 agents were focused on the problem and allegedly produced a singular solution after 88 hours, exchanging roughly 2.7 million messages and consuming at least $6.5 million in computing resources. The proposed construction involves a rotating vortex whose velocity grows without bound, which—if rigorously validated—would demonstrate finite-time blow-up rather than global smoothness.

The announcement is controversial because mathematician Tristan Buckmaster of NYU and Levent Alpöge of Anthropic had been working independently on a closely related AI-assisted approach. Their incomplete research was published shortly before OpenAI's announcement, raising questions about priority, attribution and whether ideas from their work could somehow have influenced OpenAI's models. Buckmaster has suggested that material from their research may have entered training data, while OpenAI reportedly says it cannot completely rule this out. More fundamentally, the episode raises a new question for mathematics: when AI systems build on decades of human research and then cross the final barrier to a proof or counterexample, how should mathematical credit be assigned? OpenAI has said it does not intend to claim the $1 million Millennium Prize.

Key takeaways

The Navier–Stokes problem concerns whether smooth $3$-dimensional fluid flows can develop finite-time singularities.
OpenAI claims its agents found such a singularity, which would amount to solving the Millennium problem through a counterexample to global smoothness.
The reported computation involved about 10,000 AI agents, 88 hours, 2.7 million messages, and at least $6.5 million in compute.
The result should still be regarded as a claim until the full mathematical argument is independently examined and verified.
Parallel work by Buckmaster and Alpöge has created a dispute over intellectual priority and possible influence between human research and AI training.
The case may become an important precedent for authorship, attribution and credit in AI-assisted mathematics.
OpenAI says it will not seek the $1 million Clay Mathematics Institute prize.

ARTICLE

How OpenAI Responds to Claims It Used Academics’ Work

Fri, 11 Sep 2026 19:10:08 +0300

How OpenAI Responds to Claims It Used Academics’ Work in the Navier–Stokes Breakthrough

The controversy surrounding OpenAI's claimed progress on the Navier–Stokes Millennium Prize problem has developed into a wider debate about artificial intelligence, academic credit, unpublished research, and the increasingly powerful role of AI laboratories in mathematics.
Mathematician Tristan Buckmaster and other academics have raised concerns about how OpenAI arrived at its result, particularly because Buckmaster and collaborator Levent Alpöge had themselves been working on closely related problems while using OpenAI's Codex system.
However, it is important to distinguish between the different allegations. There is currently no established evidence that OpenAI simply copied or "stole" Buckmaster and Alpöge's unpublished proof.

1. OpenAI denies using Buckmaster's private Codex work
OpenAI has issued a direct denial that Buckmaster's recent private Codex interactions contributed to the Navier–Stokes result.
According to OpenAI, an internal investigation found that Buckmaster's Codex prompts from the period before the announcement:

Quote:"could not have influenced the system in any way, including through training."

OpenAI also says that neither its researchers nor the AI agents involved in the project had access to Buckmaster and Alpöge's unpublished research before it became public.
This represents a stronger position than OpenAI initially took.
Early in the controversy, OpenAI reportedly acknowledged that it could not completely exclude the possibility that de-identified product-use data might indirectly have contributed to model improvement.
After investigating the specific case, however, OpenAI stated that the relevant Codex sessions could not have affected the model responsible for the mathematical result.
Source:
[url=https://openai.com/index/navier-stokes-solution/]OpenAI — Navier–Stokes Solution[/url]
[url=https://www.wired.com/story/openai-navier-stokes-math-discovery-academics/]WIRED — OpenAI, Navier–Stokes and academic concerns[/url]

2. OpenAI admits that news of academic progress triggered its effort
One important part of the story is not disputed.
OpenAI acknowledges that its intensive Navier–Stokes effort began after researchers at the company heard that major progress had apparently been made on a Millennium Prize problem.
The company says that on September 1 it began directing substantial AI resources toward the problem.
It later became clear that the mathematical progress being discussed involved Buckmaster and Alpöge.
This means that OpenAI is not claiming that its effort was completely unrelated to the academics' work.
Rather, its position is that hearing that progress existed encouraged OpenAI to investigate the mathematical area independently.
This creates an important distinction.
The allegation is no longer simply:

Quote:"Did OpenAI copy the unpublished proof?"

There is also a broader ethical question:

Quote:"Should an AI laboratory use information that academics are close to an important breakthrough as a signal to deploy enormous computational resources and attempt to reach the result first?"

Some mathematicians regard this as a modern form of academic "scooping", even if no confidential mathematical details were directly used.

3. OpenAI argues that the mathematical results are different
OpenAI also argues that its mathematical result is substantially different from the work carried out by Buckmaster and Alpöge.
Buckmaster and Alpöge had obtained results involving the Euler equations with external forcing.
OpenAI says its AI-assisted approach went further by finding a construction without the same external forcing, eventually producing what it claims is a route toward the Navier–Stokes problem.
If correct, this would mean that OpenAI did not simply reproduce Buckmaster and Alpöge's proof.
This part of the controversy is potentially easier for the mathematical community to evaluate, because researchers can compare the published mathematical arguments directly.

4. The dispute over academic credit
Another controversial issue concerns authorship and academic recognition.
Buckmaster has described discussions with OpenAI researchers concerning how the respective results might be presented.
According to Buckmaster, OpenAI proposed arrangements under which he could potentially be connected to OpenAI's paper, while Alpöge — who works for Anthropic — would not necessarily appear in the same way.
Buckmaster also reported a particularly tense conversation in which OpenAI researcher Sébastien Bubeck allegedly asked:

Quote:"Why would you ruin your career?"

Buckmaster interpreted the conversation as pressure.
Bubeck disputes that interpretation.
He says he was not asking Buckmaster to remove Alpöge from their own academic research. Rather, according to Bubeck, the discussion concerned authorship of OpenAI's separate work.
Bubeck has also apologized for the wording concerning Buckmaster's career, describing it as a poor choice of words rather than a threat.
Source:
[url=https://www.abc.net.au/news/2026-09-10/openai-navier-stokes-millennium-problem-claims/107132242]ABC News — Navier–Stokes dispute[/url]

5. Buckmaster has stopped short of accusing OpenAI of theft
Despite the strong reaction surrounding the controversy, Buckmaster himself has been relatively careful in his public statements.
He has said:

Quote:"I do not know whether our data was used."

He has also stated:

Quote:"I am not accusing anyone of anything."

His argument is essentially that the timeline and circumstances were unusual enough that they deserved public scrutiny.
Therefore, the statement:

Quote:"Buckmaster proved that OpenAI stole his proof"

would currently be inaccurate.
A more precise description would be:

Quote:Buckmaster raised concerns about whether unpublished AI-assisted mathematical work could have indirectly influenced OpenAI's project and questioned the way OpenAI responded after becoming aware of his team's progress.

6. Criticism from the wider mathematical community
The controversy has expanded beyond Buckmaster.
A number of mathematicians have expressed concerns about the way large AI laboratories are entering mathematical research.
An open letter associated with members of the Caltech and broader mathematics community criticized the increasing pressure to rapidly announce AI-generated mathematical discoveries.
Critics argue that AI laboratories can deploy enormous amounts of computing power after hearing that traditional researchers are approaching an important result.
Some mathematicians have also complained that the academic community is then expected to spend significant amounts of unpaid time checking extremely long AI-generated proofs.
The open letter reportedly described some of these practices as potentially amounting to:

Quote:"research misconduct."

OpenAI subsequently withdrew its sponsorship of a Caltech mathematics event following the controversy.
Sources:
[url=https://proofsandprompts.com/2026/09/10/open-letter-about-the-mathathon/]Open Letter About the Mathathon[/url]
[url=https://www.businessinsider.com/openai-caltech-ai-math-hackathon-backlash-anthropic-2026-9]Business Insider — OpenAI withdraws from Caltech math event[/url]

7. Questions about citations and attribution
A separate controversy also emerged concerning references in OpenAI's mathematical paper.
Reports stated that the original version did not properly cite earlier work by mathematicians Diego Córdoba and Luis Martínez-Zoroa, whose techniques were considered relevant to the construction.
Those references were subsequently added.
This does not demonstrate that OpenAI copied Buckmaster's research.
However, it has contributed to concerns among mathematicians that the speed of AI-generated mathematical research may sometimes come at the expense of careful attribution.
Source:
[url=https://elpais.com/tecnologia/2026-09-10/openai-corrige-de-tapadillo-su-prueba-del-milenio-para-citar-a-los-
matematicos-clave-que-ninguneo-al-anunciar-el-descubrimiento.html]El País — OpenAI adds mathematical citations[/url]

Where does the evidence currently stand?
At present, there is no publicly demonstrated evidence that OpenAI directly stole Buckmaster and Alpöge's unpublished proof.
Two important facts, however, appear to be established.

OpenAI learned that another group had made significant progress and then deliberately launched a very large computational effort toward the same general mathematical problem.
Buckmaster had been using OpenAI's Codex system while conducting unpublished mathematical research, which naturally raised questions about whether those interactions could somehow have influenced OpenAI's models.

OpenAI now says that its investigation has ruled out the second possibility for the relevant prompts.
The remaining difficulty is independent verification.
Outside mathematicians can compare the mathematical proofs themselves, but they cannot independently reconstruct OpenAI's internal training pipeline or determine precisely what information was available to every system involved.
Conclusion
The controversy therefore appears to be shifting away from the simple question:

Quote:"Did OpenAI steal Buckmaster's proof?"

OpenAI has issued a fairly specific technical denial of that allegation.
The more difficult question may instead be:

Quote:"What should happen when AI laboratories hear that academic researchers are approaching a major breakthrough and can immediately deploy thousands of AI agents and enormous computational resources toward the same target?"

That question is likely to become increasingly important as AI systems become capable of carrying out more sophisticated mathematical research.
Traditional academic norms developed in a world where competing researchers generally had comparable human limitations.
AI laboratories operate under very different conditions.
The Navier–Stokes controversy may therefore become an early example of a much larger debate about authorship, priority, research ethics and the future relationship between mathematicians and AI laboratories.

EMS statement on recent Navier–Stokes announcement

Thu, 10 Sep 2026 19:23:49 +0300

The European Mathematical Society (EMS) has issued a statement on OpenAI’s recent announcement concerning the Navier–Stokes Millennium Prize Problem. The EMS describes the development as potentially a historic milestone in mathematics, both because a major open problem may have been resolved and because the work emerged from collaboration between professional mathematicians and AI systems.

However, the Society stresses that the result did not arise independently of existing mathematics: it builds closely on ideas developed by Diego Córdoba, Luis Martínez-Zoroa, and Fan Zheng, as well as recent progress by Levent Alpöge and Tristan Buckmaster, together with decades of earlier research.

The EMS considers the speed of the human–AI collaboration remarkable, but says the episode raises important questions about authorship, attribution, and scientific credit when mathematics is produced jointly by humans and machines. It also expresses concern that the AI model used by OpenAI is internal and not generally accessible, arguing that unequal access to powerful research systems could conflict with principles of open science and equal opportunity. Despite these concerns, the EMS concludes by joining in the admiration and celebration of the achievement while emphasizing that the mathematical community will need to develop new norms for AI-assisted research.

Key takeaways

The EMS regards the announcement as a potentially historic mathematical achievement.
It explicitly credits earlier mathematicians whose ideas underpin the approach.
Human–AI collaboration appears to have accelerated the research dramatically.
New rules may be needed for authorship and credit in AI-assisted mathematics.
The EMS is concerned that OpenAI's research model is not openly accessible.
Its overall position is supportive but cautious: celebrate the mathematics while addressing the scientific and ethical consequences.

ARTICLE

Has AI cracked a $1m maths problem?

Thu, 10 Sep 2026 04:51:08 +0300

Has AI cracked a $1m maths problem?

The Plus Magazine article discusses OpenAI’s September 2026 announcement that an internal AI system had produced a proposed solution to the Navier–Stokes existence and smoothness Millennium Prize Problem, one of the seven problems for which the Clay Mathematics Institute offered a $1$ million prize. The Navier–Stokes equations describe the motion of fluids such as air and water and underpin applications ranging from weather prediction to aerodynamics. The fundamental mathematical question is whether initially smooth three-dimensional solutions must remain smooth forever, or whether they can develop a singularity in finite time.

OpenAI says its system constructed a smooth, finite-energy solution with smooth external forcing in which the velocity becomes unbounded after a finite time. In other words, rather than proving that smooth solutions always exist, the proposed proof takes the opposite route: it constructs a situation in which the Navier–Stokes dynamics blow up. OpenAI states that this establishes cases C and D of the official Millennium Problem formulation, and it released both a conventional mathematical proof and a formalized version checked in Lean.

However, Plus deliberately frames the development as something the mathematical community is still checking and debating, rather than simply declaring the Millennium Problem permanently settled. There is also controversy over attribution and the relationship between OpenAI's work and related research by Tristan Buckmaster, Levent Alpöge and earlier work by Diego Córdoba and Luis Martínez-Zoroa. Buckmaster stresses that important ideas behind the forced-blowup approach arose from this earlier human research and describes extensive collaboration between mathematicians and LLMs. The article also emphasizes that even if the proof is accepted, ordinary engineering applications are not suddenly invalidated: the pathological solutions do not mean aircraft simulations or weather models will cease to work.

Key takeaways

OpenAI has presented a claimed solution of the Navier–Stokes Millennium Prize Problem by demonstrating finite-time singularity formation rather than universal smoothness.
The result comes with both a traditional proof and a Lean-formalized proof, giving the claim an unusually strong form of machine verification, though broader mathematical scrutiny is still underway.
The story is also about AI's rapidly changing role in mathematics: AI systems are moving from assisting mathematicians to potentially producing major original proofs.
For now, it is safest to say that AI has produced a serious proposed resolution of the $1$ million problem—not that the Clay Mathematics Institute has already officially awarded or certified the prize.

ARTICLE

AI Has Solved One of Math’s $1 Million Millennium Prize Problems

Wed, 09 Sep 2026 01:24:56 +0300

Summary

In a potentially historic development, OpenAI researchers announced on September 8, 2026 that an AI system had produced a proof of finite-time singularity formation for the three-dimensional Navier–Stokes equations, one of the seven Millennium Prize Problems. These equations describe the motion of incompressible fluids and can be written schematically as
$\displaystyle \frac{\partial u}{\partial t}+(u\cdot\nabla)u=-\nabla p+\nu\Delta u+f,$
together with the incompressibility condition
$\displaystyle \nabla\cdot u=0.$

The central question has been whether initially smooth solutions must remain smooth forever or whether they can develop a singularity, where some quantity associated with the velocity field becomes unbounded in finite time. According to OpenAI, its construction produces such a blow-up starting from smooth data while using a smooth external force and keeping the relevant energy finite. If the argument survives full mathematical scrutiny, it would settle the Millennium problem by demonstrating that global regularity can fail.

The breakthrough did not arise from AI in isolation. Quanta emphasizes the crucial earlier work of Diego Córdoba and Luis Martínez-Zoroa, who developed an unusual analytic method based on an infinite cascade of individually regular fluid structures. Their previous constructions could create singularities but did not satisfy all the smoothness requirements imposed on the forcing term. The remaining challenge was therefore to make the cascade produce blow-up while the forcing remained sufficiently smooth. OpenAI reports that roughly 10,000 autonomous AI agents explored the problem in parallel and eventually discovered a construction satisfying these additional conditions. The resulting argument was subsequently formalized in Lean, allowing its logical steps to be machine-checked.

The result is also surrounded by important questions concerning mathematical priority and attribution. Shortly before OpenAI's announcement, mathematician Tristan Buckmaster and Anthropic researcher Levent Alpöge announced related AI-assisted progress for Euler-type fluid equations, also building on ideas developed by Córdoba and Martínez-Zoroa. The episode therefore raises a new question for mathematics: when an AI system completes a proof whose conceptual framework was created by human mathematicians, how should intellectual credit be distributed?

Another important distinction is that formal verification is not automatically identical to independent mathematical acceptance. Lean can verify that a formal theorem logically follows from its stated assumptions, but mathematicians must still check that the formalized statement corresponds precisely to the Navier–Stokes problem posed by the Clay Mathematics Institute. The wider mathematical community must also examine the construction, its hypotheses, and the relationship between the formal theorem and the original Millennium Prize formulation.

Key takeaways

Claimed result: A smooth three-dimensional Navier–Stokes solution can develop a finite-time singularity under the permitted smooth forcing conditions.
The mathematical system studied is

$\displaystyle \frac{\partial u}{\partial t}+(u\cdot\nabla)u=-\nabla p+\nu\Delta u+f,$
with
$\displaystyle \nabla\cdot u=0.$

AI played an unprecedented role: thousands of autonomous agents searched through possible arguments and constructions, with the final proof subsequently formalized in Lean.
Human mathematics remained fundamental: the breakthrough relies heavily on the earlier infinite-cascade ideas developed by Córdoba and Martínez-Zoroa.
The $1 million prize has not automatically been awarded. The Clay Mathematics Institute has its own requirements for recognition and independent verification before a Millennium Prize solution can be officially accepted.
If the proof withstands independent scrutiny, it would represent one of the most important demonstrations so far that AI can contribute not merely to checking mathematics but to producing genuinely new research-level mathematical arguments.

OpenAI has presented a formally verified candidate solution to the Navier–Stokes Millennium Prize Problem. If independent mathematicians confirm that the argument satisfies the exact Clay conditions, it could constitute the solution of one of mathematics' most famous open problems.

ARTICLE / ARTICLE [PDF]

OpenAI claims a solution to Navier-Stokes Millennium Prize Problem

Tue, 08 Sep 2026 22:11:13 +0300

OpenAI and the Navier–Stokes Millennium Prize Problem
A proposed AI-generated solution to one of mathematics’ greatest open problems

OpenAI has announced a proposed solution to the famous Navier–Stokes existence and smoothness problem, one of the seven Millennium Prize Problems established by the Clay Mathematics Institute.
The three-dimensional incompressible Navier–Stokes equations describing the motion of a viscous fluid are
$\partial_t u+(u\cdot\nabla)u-\nu\Delta u+\nabla p=f,\qquad \nabla\cdot u=0.$
Here $u$ represents the velocity of the fluid, $p$ its pressure, $\nu>0$ the viscosity and $f$ an external force.

The central mathematical problem
One of the fundamental questions in mathematical fluid dynamics is whether a solution that begins smoothly must remain smooth for all time.
Alternatively, could the equations produce a finite-time singularity, where some quantity associated with the velocity of the fluid becomes infinite after a finite amount of time?
OpenAI's proposed proof takes the second route.
According to the paper, for every viscosity $\nu>0$ it is possible to construct a smooth, compactly supported external force $f$ and a solution starting from rest,
$u(\cdot,0)=0,$
such that its total kinetic energy remains bounded:
$\sup_{0\le t<1}|u(t)|_{L^2}<\infty,$
while at the same time the maximum magnitude of the velocity becomes unbounded as $t$ approaches $1$:
$\limsup_{t\to1^-}|u(t)|_{L^\infty}=\infty.$
In other words, the fluid can retain finite total energy while its velocity becomes arbitrarily large in an increasingly small region of space.

What does the singularity look like?
The construction can be pictured as an extremely thin and increasingly stretched vortex.
As time progresses, the vortex becomes concentrated into a smaller region, spirals inward and accelerates. Its local velocity grows without bound, even though the total kinetic energy of the fluid remains finite.
A crucial part of the proof is arranging a delicate cancellation between several terms in the Navier–Stokes equations — nonlinear acceleration, pressure and viscosity — so that the external forcing term $f$ itself remains perfectly smooth.
The singular behaviour therefore appears in the velocity field rather than being introduced artificially through a singular external force.

The role of artificial intelligence
Perhaps the most remarkable aspect of the announcement is the way in which OpenAI says the proof was discovered.
According to OpenAI, a large multi-agent AI research system explored many different mathematical approaches simultaneously. The system first investigated a related finite-time blow-up problem for the inviscid Euler equations and subsequently concentrated its effort on the Navier–Stokes equations.
The resulting mathematical argument was also subjected to formal verification using Lean, a proof assistant increasingly used for computer-verified mathematics.
If the result is confirmed, the achievement would therefore be important not only for fluid mechanics and partial differential equations, but also for the emerging field of AI-assisted mathematical research.

Has the Millennium Prize Problem officially been solved?
Not yet.
At present, the result should be described as a proposed solution.
Even a very detailed proof, together with computer formalization, does not automatically settle a Millennium Prize Problem. The argument must be examined carefully by independent specialists and eventually gain broad acceptance within the mathematical community.
The Clay Mathematics Institute also requires a substantial period of public mathematical scrutiny before formally considering a solution for the Millennium Prize.
Therefore the most important stage now begins: mathematicians working in partial differential equations and fluid dynamics must check every part of the construction independently.

Why this matters
If the proof survives independent verification, the consequences would be profound.
It would show that smooth solutions of the forced three-dimensional Navier–Stokes equations can develop finite-time singularities, answering one of the most famous questions in modern mathematical analysis.
It would also represent an extraordinary milestone in the relationship between mathematics and artificial intelligence: an AI research system would have contributed directly to resolving a problem that has resisted generations of mathematicians.
For the moment, however, the correct mathematical attitude is one of great interest combined with careful verification.
The proposed proof may ultimately become a historic breakthrough — but its validity will be determined by the mathematical community.

Source:
ARTICLE

Formalizing Fermat's Last Theorem

Sat, 05 Sep 2026 15:09:30 +0300

Formalizing Fermat’s Last Theorem — Anthropic, September 4, 2026
Anthropic reports what it describes as the first complete computer-checked formal proof of Fermat’s Last Theorem (FLT). The theorem states that there are no positive integers $a,b,c$ satisfying
$a^n+b^n=c^n$
for any integer $n>2$. Andrew Wiles, later working with Richard Taylor, proved FLT in the 1990s using deep results connecting elliptic curves and modular forms. Anthropic’s achievement is not a new mathematical proof of FLT, but a formalization of the existing mathematical argument in the Lean proof assistant, where every logical step can be checked mechanically. According to Anthropic, Claude worked largely autonomously for 11 days, generated about 13 million lines of Lean code, and proved roughly 30,300 intermediate theorems.

The project used a multi-agent system together with Prove2Me, a collaborative formalization platform that organizes mathematical dependencies as a directed acyclic graph. Different Claude agents could therefore work simultaneously on algebra, number theory, geometry, harmonic analysis, and other components of the proof. The final argument follows a streamlined exposition of Wiles’s proof by Henri Darmon, Fred Diamond and Richard Taylor. The finished proof was compiled and verified by Lean, demonstrating that a modern AI system can formalize mathematics at a scale that previously required enormous amounts of specialized human effort.

The broader significance may extend well beyond Fermat’s Last Theorem. Formalizing advanced mathematics is difficult because proof assistants require every intermediate logical step that ordinary mathematical writing often leaves implicit. AI systems could substantially reduce this burden, making it practical for research papers to be accompanied by machine-verifiable proofs. This could help detect subtle errors in existing mathematics and provide an increasingly important mechanism for checking mathematical arguments generated by AI itself. Formal verification, however, should complement rather than replace clear, human-readable mathematical proofs.

Key takeaways

Claude did not discover a new proof of FLT; it formalized an existing proof so that Lean could verify it mechanically.
Fermat’s Last Theorem states that $a^n+b^n=c^n$ has no positive integer solutions when $n>2$.
The project involved about 13 million lines of Lean code and roughly 30,300 proved intermediate theorems.
The major breakthrough is in AI-assisted mathematical formalization and verification, potentially making machine-checked research mathematics much more practical.

ARTICLE

Formalizing 100 Theorems

Fri, 04 Sep 2026 23:34:23 +0300

The “Formalizing 100 Theorems” project, maintained by mathematician and computer scientist Freek Wiedijk, tracks the progress of formalizing a well-known “Top 100” list of important mathematical theorems using computer proof assistants. A formalized theorem is not merely written as an ordinary mathematical proof: every definition, logical step, and inference is encoded in a rigorous formal language so that a proof-checking system can verify it mechanically. The list ranges from classical results such as the irrationality of $\sqrt{2}$, the Pythagorean theorem, and the infinitude of primes to much deeper results such as Gödel’s incompleteness theorem, the Prime Number Theorem, quadratic reciprocity, and the Fundamental Theorem of Algebra. According to the current project page, 99% of the 100 theorems have now been formalized in at least one system.

The project also serves as an informal benchmark for comparing major interactive theorem provers and formal mathematics libraries. It records which systems have formalizations for each theorem, including HOL Light (95 theorems), Isabelle (92), Lean (82), Rocq/Coq (80), Metamath (74), Mizar (71), ACL2 (48), and ProofPower (43), among others. The aim is not to catalogue every existing proof but to show how broadly different proof assistants can handle substantial mathematics. In this sense, the project documents the remarkable growth of formal mathematics: results that traditionally existed only as human-readable arguments are increasingly being converted into completely machine-verifiable proofs, laying important foundations for computer-assisted mathematics and, increasingly, AI-assisted theorem proving. [/url]

[url=https://www.cs.ru.nl/~freek/100/]PROJECT

Fermat's Last Theorem in Lean 4

Fri, 04 Sep 2026 22:58:40 +0300

Anthropic’s Fermat’s Last Theorem project is a large formalization of Fermat’s Last Theorem in Lean 4. It encodes the modern proof developed through the work of Frey, Serre, Ribet, Wiles, and Taylor–Wiles, showing formally that for integers $n \ge 3$ and positive natural numbers $a,b,c$, the equation $a^n+b^n=c^n$ has no solutions. The repository contains more than 60,000 Lean modules and nearly 30,000 formally stated theorems, together with an offline HTML interface for exploring the proof and its dependencies. Much of the Lean code was produced by AI agents building on existing human-written formal mathematics from projects such as Mathlib and the Imperial College London FLT project.

The significance of the project is not that it introduces a new proof of Fermat’s Last Theorem, but that it makes the established proof machine-checkable at a very deep level. Anthropic reports verifying the result through a complete Lean build, the Lean comparator tool, and nanoda, an independently implemented Lean kernel written in Rust. The final theorem uses only Lean’s standard axioms and contains no unfinished proofs or unsafe shortcuts. The project therefore serves as an important demonstration of how AI can assist with the formalization of extremely advanced mathematics while leaving the Lean kernel responsible for checking the logical correctness of every step.

PROJECT

Prime Gaps at Most 186

Thu, 03 Sep 2026 22:50:11 +0300

Quote:
New result by OpenAI on Prime gaps

Summary
OpenAI’s PrimeGaps186 repository presents a Lean 4 formalization of a result on bounded gaps between prime numbers, together with a Python program that checks the necessary numerical estimates. The target theorem is
$\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186$,
meaning that there are infinitely many pairs of consecutive primes whose difference is at most 186. The proof proceeds by establishing the sieve-theoretic statement $\mathrm{DHL}[40,2]$: every admissible collection of 40 integer shifts has infinitely many translates containing at least two primes. An explicit admissible 40-element tuple of diameter $186$ then yields the stated bound.

The important qualification is that this is not a completely self-contained formal proof of the prime-gap theorem in Lean. The Lean development relies on three explicit assumptions. Two concern deep estimates for Kloosterman-type exponential sums, derived from established work by Deligne/Katz and Fouvry–Kowalski–Michel. The third consists of a substantial collection of numerical integral bounds. These results are mathematically known or computationally checked, but they have not themselves been formally proved inside Lean. The accompanying Python certificate recomputes the numerical part and verifies that the required bounds pass, but successfully running it does not eliminate the corresponding Lean axiom.

What makes the project particularly interesting is its combination of analytic number theory, rigorous numerical computation, and formal verification. The Lean kernel has checked the logical deductions from the stated assumptions, and the numerical certificate provides an independently reproducible computational check. Thus the repository should be understood as a conditional machine-verified formalization of the bound $186$, rather than as a new unconditional proof of a previously unknown prime-gap result. It is also a useful example of how advanced mathematical arguments can be split into formally verified reasoning, literature-backed theorems, and certified computation.

Key takeaways

Main result: $\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186$.
It formalizes the implication $\mathrm{DHL}[40,2]\Rightarrow$ infinitely many prime gaps $\le 186$.
The Lean proof is conditional on three explicit axioms; therefore it is not yet a fully formalized end-to-end proof.
A Python certificate verifies the large numerical component independently.
The project illustrates a promising model for combining AI-assisted/formal mathematics, Lean, numerical certification, and classical analytic number theory.

In simple terms: the interesting achievement is not discovering that prime gaps can be bounded by $186$, but showing how a sophisticated prime-gap argument can be turned into a largely machine-checkable mathematical object, with the remaining unformalized assumptions clearly isolated.

ARTICLE