Transformation

It seems like every odd number greater than 5 can be written as the sum of three primes. (They don’t have to be distinct: 11 = 3 + 3 + 5.) Harald Helfgott, a senior researcher at France’s National Center for Scientific Research, claimed to have proved this result, known as the ternary Goldbach conjecture, in 2013. Yet there were some issues with the initial proof. Helfgott believed he had fixed them, but his argument would eventually stretch across more than 500 pages. That’s a lot of math to check.

This type of dilemma is why formal proofs exist. Formal proofs reduce every line of mathematical argument to extremely basic steps — so basic that a computer can verify each small step in a mechanistic way. The idea is to remove expertise and persuasion from the picture, and in so doing, to eliminate the possibility of mistakes. “Formalizing” a proof like this has been a tedious and time-consuming process. It also required significant mathematical expertise to make sure it was done correctly. (The nuances here are chronicled by longtime Quanta Magazine contributor Kevin Harnett in his book “The Proof in the Code.”)

Over the past few years, a central goal of the AI-for-math community has been to figure out how to use AI systems to translate ordinary mathematical arguments into formally verifiable code. If this process of “autoformalization” succeeds, it gives AI models the ability to check their own work. But autoformalization had been suffering from the same accuracy problems that plagued other AI outputs. For instance, a May paper from Meta that claimed to formalize 26 math textbooks was riddled with errors.

Like so much else, AI autoformalization capabilities changed in the summer of 2026. In early September, Anthropic announced that they had formalized the proof of Fermat’s Last Theorem. It took a swarm of agents 11 days to do so; they produced some 13 million lines of computer code. Unlike the Meta paper, experts concluded that the autoformalization worked. “If thousands of pages of the literature can be formalized end-to-end by some kind of AI swarm in an 11 day period now, then in the future we will start to see formalization of modern research being done on the fly,” wrote Kevin Buzzard, a formalization expert at Imperial College London. As if to prove his point, Anthropic researchers announced on November 9 that what had taken 11 days in September can now be done in 30 hours.

About a third of OpenAI’s October 6 announcement of hundreds of results were accompanied by formal proofs. Since then, there have been increasing efforts to formalize not only particular results, but also entire bodies of knowledge. Beginning last week, an AI startup called Axiom Math announced four autoformalization results in rapid succession:

• The formalization of the classification of finite simple groups, an enormous effort spanning tens of thousands of pages over many years, that no human had fully understood.
• A huge open-source textbook of modern algebraic geometry written by Aise Johan de Jong of Columbia University, called the Stacks Project.
• The Weil conjectures, precursors to the Langlands program, which is central to modern math.
• The first seven chapters of a textbook on cluster algebras.

Independent experts say they are satisfied with Axiom’s formalizations. “They have done impressive things,” said Johan Commelin, the director of the Mathlib Initiative, a key formalization effort. While formalizing the classification of finite simple groups, Axiom say they found 96 (minor and correctable) errors in 47 published papers.

And as for Helfgott’s proof of the ternary Goldbach conjecture, it too, has been formally verified, as of November 10. As Jared Duker Lichtman of Stanford University put it in an email to me, “This is huge!!”

It now seems a question not of if, but when, all of human mathematical knowledge will be formalized by AI.

In other news:

Physical Superintelligence, a startup, announced a proof of an important conjecture in quantum computing formulated by Scott Aaronson and Andris Ambainis in 2009. Aaronson expressed mixed feelings about this on his blog.

The “shepherd’s group” of eminent physicists vetting OpenAI’s 1,147-page manuscript in quantum field theory published formalizations of the claimed results. This has followed weeks of closed-door scrutiny by the physicists amid calls from some mathematicians for their immediate release.

Elliot Glazer, a logician at Epoch AI, announced the existence of a polynomial with 292,890,231,905 variables with integer coefficients with the following properties: If all but one of the variables are rational numbers (fractions) and the polynomial equals 0, the last remaining variable is guaranteed to be an integer. And for any integer, you can always find a combination of fractions for the other variables that make the polynomial compute to 0. His announcement provoked a great deal of controversy. Glazer and others subsequently found much smaller polynomials with the same properties.

From the Quanta archives:

OpenAI’s result number 160 was about the growth rate of van der Waerden numbers, which appear in Ramsey theory, the study of unavoidable patterns. In 2021, Erica Klarreich wrote about their surprising behavior. In 2023, Anna Kramer explained how they can be used in a deliberately arcane way to prove that the primes are infinite. And in 2022, Leila Sloman wrote about a different conjecture by Bartel Leendert van der Waerden, for whom the numbers are named.

The OpenAI proof dump in early October included a landmark result in number theory: a claimed proof that so-called “Landau-Siegel zeros” do not exist. It was overshadowed by the company’s proof of the generalized quasi-Riemann hypothesis, which automatically implied the nonexistence of these special zeros. But the Landau-Siegel zero result is significant in and of itself.

Mathematicians probe patterns in the prime numbers using the so-called zeta function. To then study patterns in how the primes interact with other numbers, they look at L-functions, which are generalizations of the zeta function. Both the Landau-Siegel and generalized quasi-Riemann problems are about particular L-functions that are important in number theory. In essence, Landau-Siegel is about how prime numbers behave. As Andrew Granville of the University of Montreal put it, “What Siegel zeros say is, something crazy happens.”

The inputs to L-functions are complex numbers, each of which has two parts: a real part, and an imaginary one (a multiple of the square root of –1, which mathematicians call i). The generalized Riemann hypothesis posits that, with some trivial exceptions, these L-functions equal zero only when their input has a real part of 1/2. (The “quasi” version is less strict.)

If the generalized Riemann hypothesis turns out to be false, it would mean some other zeros might exist. The farther a would-be zero is from having a real part of 1/2, the bigger a disruption it would cause to how prime numbers are expected to behave. That’s where Landau-Siegel zeros come in. These are putative zeros that have an imaginary part of 0 and a real part very close to 1 (which is, in the context of this problem, very far away from 1/2). This makes these zeros particularly important.

Mathematicians have long known that the zeta function itself does not have Landau-Siegel zeros. But even though numerical checks made it seem unlikely, no one could rule out the possibility that certain other L-functions might. If such zeros existed, that fact could be used to prove many other important results — including the twin primes conjecture, which says that there are an infinite number of prime numbers that differ by 2 (such as 11 and 13, or 17 and 19). “If you have a Siegel zero, then other things fall into place in an unexpected way,” said Granville.

“It’s all moot now,” he added.

In the weeks since OpenAI released its proof that Landau-Siegel zeros do not exist, mathematicians have been posting ever-simpler versions of the result.

One reformulation, by Ben Green of the University of Oxford, is, as Terence Tao wrote, “particularly elegant.” Green obtained his proof through conversations with OpenAI’s Astra model, and demurs that “no human originality is claimed.” Jacob Pescador, Kevin Barreto, and Roelof van Dijk have used both Astra and Anthropic’s Opus 5.5 to further tweak Green’s reformulation.

“I generally won’t read AI papers directly,” said Bryce Kerr of the University of New South Wales in Canberra, who assembled one of the other re-proofs of the Siegel result. “My process starts with asking AI to explain the new ideas or ‘big picture’ then I’ll try to fill in the details myself. If I get stuck I’ll go back to AI and ask it more questions. I guess it’s analogous to asking a human author to explain one of their papers.”

In place of the old races around priority, there appears to be an emerging competition to see who can devise the shortest, simplest proof. Barreto’s version weighs in at just three pages. “People are thinking I was trying to optimise for page count,” wrote Barreto, who is an undergraduate at the University of Cambridge. “I was trying to optimise for more elementary classical machinery, which so happened to shorten the proof as a consequence.”

Granville, who is 64 years old, said that for many number theorists of his generation, the Riemann hypothesis always seemed too daunting a goal. But he and others had spent decades trying and failing to prove that Landau-Siegel zeros don’t exist. “For me,” he said, seeing the proof, “it’s quite emotional, more so in some ways than the quasi-Riemann hypothesis, because it’s what I really tried to do.”

In Other News

Thirty-two mathematicians who met at Harvard’s Center for Mathematical Sciences and Applications published a report on Math Research in the Age of AI. How research is done is changing so quickly, the report said, that math departments “may consider allowing research statements without any mention of future research plans” when reviewing potential promotions and new hires.

The Academy for the Mathematical Sciences, based in Cambridge, England, issued another report on how AI is affecting both pure and applied math, systematically laying out AI opportunities, risks, and measures to mitigate those risks.

From the Quanta Archive

In David Hilbert’s list of 23 problems for the 20th century, Number 10 asked if there was a way to tell if any polynomial equation with integer coefficients had integer solutions. In 1970, Yuri Matiyasevich showed that no such algorithm exists. But what happens when you allow solutions to be rational numbers? OpenAI claims to have resolved this version of the problem, too. Joseph Howlett wrote about generalizations of Hilbert’s 10th problem in 2025. In 2021, Stephen Ornes wrote about Hilbert’s related 13th problem. And Kevin Hartnett wrote about patterns in rational solutions to polynomial equations in 2017.

On October 26, OpenAI announced that an advanced AI model had solved three major problems: one in math, one in theoretical computer science, and one in physics. On the advice of experts in the relevant areas, the company released the results in very different ways.

The math result, a proof of the “local smoothing conjecture,” was simply posted online, together with a Lean verification. The idea is to give as many people as possible an equal shot at making heads or tails of the AI’s output, which often appears unintelligible, even to experts.

The computer science result — which disproved a major conjecture, to the surprise of many — was also immediately released, but this time with a promise that it would be “verified and shepherded” by three leading researchers in the field. Hours later, Anthropic independently released their own version of the result.

On the advice of a group of physicists led by David Gross, a Nobel Prize–winning physicist, OpenAI hasn’t yet released their third result, which claims to make a theory in particle physics mathematically rigorous. Instead, the physicists are now working to understand the 1,147-page AI proof themselves. Meanwhile, Levent Alpöge of Anthropic and Ethan Sussman, a postdoctoral fellow at Northwestern University, have released work in progress on related questions.

“In our view, these manuscripts are best understood as a form of raw research data,” OpenAI wrote. Each approach to converting that “raw data” into human understanding has pros and cons; it’s not clear if one of these approaches (or something new entirely) will emerge as a new norm for how to disseminate AI-generated claims in math and science.

For now, here’s a bit more detail about each of the three claims:

Proof of the Local Smoothing Conjecture

First described by Christopher Sogge in a 1991 paper, the local smoothing conjecture is about how waves like light and sound behave. It posits that as waves spread, they can’t concentrate too much energy in too small of a space for too long of a time.

To show this, mathematicians need to analyze solutions to the wave equation, a partial differential equation that looks simple but is hard to study. In 2019, Hong Wang (who won a Fields medal earlier this year) and two collaborators proved the local smoothing conjecture in two dimensions. OpenAI claims to have proved it in all dimensions.

The conjecture stands at the top of a tower of important conjectures in harmonic analysis. The new proof automatically implies that these conjectures are also true. The tower includes the Kakeya conjecture, a statement about how much maneuvering room is needed to get a needle to point in every possible direction. The new result would prove that the Kakeya conjecture is true in all dimensions.

Disproof of the Exponential Time Hypothesis

Logical formulas combine inputs, each of which can be either true or false, with NOT, OR, and AND statements. (If X is true and Y is false, then “X AND Y” is false, but “X OR Y” is true.) A formula is said to be “satisfiable” if there is a combination of inputs for which the formula as a whole is true. (The previous examples are satisfiable; “X AND Y” is true when both X and Y are true. However, “X AND NOT X” is unsatisfiable — there’s no input X that gives a true output.)

For small numbers of inputs, it’s simple enough to figure out if a formula is satisfiable or not. But if there are many different inputs, it can take a long time to do so. The exponential time hypothesis (ETH) concerns how much time algorithms need to figure this out for formulas that follow a particular format.

The ETH posited that such algorithms had to perform badly in a precise sense. Finding a faster algorithm would allow you to find faster algorithms for many other problems, but computer scientists largely expected that to be impossible.

Anthropic and OpenAI have now refuted the hypothesis, finding algorithms that perform faster than the hypothesized limit when there’s an extremely large number of variables. Researchers next hope to explore whether the result will lead to progress on the broader “P = NP” problem, which is arguably the most important question in theoretical computer science.

Proof That Quantum Field Theories Are Consistent

For decades, physicists have built the so-called Standard Model of particle physics on math that is not fully rigorous. To firm up that foundation, one of the Millennium Prize Problems calls for a proof of two statements. First, that certain key mathematical elements of the Standard Model are rigorously consistent. And second, that the size of the lightest possible particle in the Standard Model with nonzero mass must have some fixed lower bound — its mass can’t be arbitrarily small. (This property is called the mass gap.) The unreleased OpenAI manuscript and work-in-progress from Sussman and Alpöge claim to prove the first statement, but not (as of yet) the second.

From the Quanta Archives

Out of the hundreds of results that OpenAI announced in its proof dump earlier this month, it shared “reasoning traces” — which explain how their AI model found what it found — for only ten of them. One of those ten was a proof that approximating π with fractions is as hard as it can possibly be.

In 2025, Erica Klarreich wrote about the difficulty of proving that numbers are irrational. In 2019, Kevin Hartnett wrote about how to approximate π with fractions; Patrick Honner followed up with an exposition of how to approximate the square root of 2. In 2023, David Richeson wrote about Liouville numbers, irrational numbers that can be approximated very well by fractions.

One day in August, Caiman Moreno-Earle, a 19-year-old sophomore at the California Institute of Technology, had an idea. As Brian Zhao, a fellow student, remembers it, Moreno-Earle asked, “What if we give ourselves AI and lock ourselves in a basement for 40 hours and try and solve some open problems?” Almost on a lark, the pair, together with a few other students, asked Anthropic for $1 million in computing credits, expecting the tech company to come back with a counteroffer of something like $50,000. But Anthropic surprised them by agreeing to their original ask. Shortly afterward, OpenAI pledged a matching sum. A slew of other startups and tech companies also pledged support.

Later that month, the students launched a spare website devoted to what they decided to call the “Caltech Mathathon.” They planned for 100 teams to compete to “solve open conjectures and build new mathematical theories” in “the first hackathon ever devoted to research level mathematics.” In their vision, students would use AI to speed up the process of coming up with new ideas and bringing them to maturity.

Almost immediately, they ran into opposition. An open letter criticizing the event, drafted by Tasmin Chu, a Caltech graduate student, quickly attracted several thousand signatures. “This event is likely to have destructive impacts for the mathematical community,” the letter read.

The signatories worried that “AI companies will take credit for the effort of talented undergrads,” and that the Mathathon would lead to a slew of mathematical slop. They called on the organizers to suspend the event.

Then something surprising happened. Sergei Gukov, a professor at Caltech, and Terence Tao of UCLA, who has become an éminence grise at the junction of AI and mathematics, got the organizers of the Mathathon (mostly undergraduates) and some of the signatories on the open letter (largely graduate students) to start talking to each other. “Everybody involved wants to move mathematics forward, so actually there was less disagreement between them than might initially have been reported,” Tao said in an email.

“We realized you didn’t have to solve an open problem to push mathematics forward,” said Zhao. And so, at the suggestion of Mayla Ward, a Caltech graduate student who had signed the open letter, they began thinking about how to refocus the event on finding new proofs for old results.

As the two sides were beginning their discussions, OpenAI abruptly dropped its sponsorship. Shortly thereafter, Anthropic and the Mathathon organizers mutually decided to part ways. The Society for Artificial Intelligence Research, a nonprofit led by Tao, and XTX Markets, an algorithmic trading firm, stepped in to provide logistical support and funding. By late September, the two sides issued a joint statement on Tao’s blog announcing the new format. They plan to publicly release a list of problems, give participants 40 hours to work on them “hackathon style,” and then have some of the teams spend the next two months revising and writing up their results with mentors.

Zhao has begun compiling a list of some existing proofs that are long and hard to understand. (One, at more than 250 pages, takes up the entire Fall 1963 issue of the Pacific Journal of Mathematics.) “We want to heal the community through this event instead of dividing it,” he said. “It’s clear there is a big divide: Two thousand mathematicians signed the open letter against the Mathathon; on the other hand, 2,000 applied to be participants and judges.”

The revamped event will be held in mid-November.

In Other News

Grant Sanderson of the YouTube channel 3Blue1Brown released a video in which he made the case that it’s never been a better time to become a mathematician.

A group of mathematicians published an essay about “How to Formalize All of Mathematics.”

From the Quanta Archives

The Kakeya conjecture asks how much space you need to maneuver a needle in many different directions. (It’s harder than it sounds.) It can be posed in different number systems and different dimensions. OpenAI’s October 6 release included claimed proofs of the conjecture in two such settings.

Earlier this year, Natalie Wolchover profiled Hong Wang after she was awarded a Fields medal in large part for her proof (with collaborator Joshua Zahl) of the standard 3D version of the conjecture. Joseph Howlett wrote about their proof in 2025, and Emily Buder made a related video. Jordana Cepelewicz reported on the conjecture’s implications; Patrick Honer explained some of the ideas behind the problem; and Kevin Hartnett wrote about how it works in other number systems.

When OpenAI released their 377 results on October 6, it was clear that many were major breakthroughs. But one stood out: a proof of the “quasi-Riemann” hypothesis, a weaker version of the Riemann hypothesis, arguably math’s biggest open problem. Though poorly written, the new proof is, according to Jared Duker Lichtman of Stanford University, “the most significant AI-for-math achievement so far, by quite a margin.”

We wrote about the result, the surprising techniques that the proof uses, and why the ramifications are so consequential. You can read that story here.

In Other News

The First Proof Project — an effort to test the mathematical abilities of AI models by using carefully curated sets of problems — announced the results of their third round of trials last week. They found that frontier models from OpenAI and Anthropic far outperformed open-source alternatives, but that all the models they tested were bad at writing up their results and properly citing sources.

From the Archives

As mathematicians parse the hundreds of claimed proofs from OpenAI, we will resurface Quanta stories that help explain the ideas in question. In 2021, Alex Kontorovich explained what the Riemann hypothesis is in a video and accompanying essay. In 2022, Leila Sloman wrote about work by Alexander Dunn and Maksym Radziwiłł that pioneered techniques used in OpenAI’s quasi-Riemann proofs. And in 2024, Jordana Cepelewicz wrote about James Maynard and Larry Guth’s proof establishing a new cap on exceptions to the Riemann hypothesis.

Mathematicians have started to take stock of the 377 claimed proofs that OpenAI released on Tuesday, October 6 — although the task will likely require months if not years.

The 722 accompanying papers, which span the entirety of modern math, theoretical computer science, and mathematical physics, appear to be of varying quality. Many seem to contain remarkable resolutions to long-standing challenges. However, the technology company has already withdrawn three of the papers, in the area of algebraic geometry, due to a misplaced minus sign. Mathematicians are poring over the remaining 719, some with excitement and others with frustration.

“We’re now expected to either (i) check all this garbage that OAI is producing or (ii) concede that all of these conjectures have been proven,” one algebraic topologist wrote to me. “I believe in politics this is known as ‘flooding the zone.’ We simply don’t have the resources to correct the record.”

OpenAI is claiming formal verification — that is, a guarantee of correctness using code written in a programming language called Lean — for some 42% of the papers (and climbing). But the formalizations do not appear to be ironclad. A handful of the Lean statements had technical issues. Though these could be easily fixed, the errors point to the fact that the mere existence of a Lean proof is not the final word.

Furthermore, to verify a proof in Lean, one needs to translate the mathematical statement being proved into an equivalent statement in Lean code. “That’s not something that can be established automatically, it needs human experts to read the Lean code,” said Johan Commelin, the director of the Mathlib Initiative, which maintains a digital library of proofs that have already been formalized. Commelin added that though he has not confirmed this firsthand, “some of the formalizations [appear to] prove weaker statements than what’s claimed in the paper. Or only formalize parts of the result claimed on paper.”

Other papers, meanwhile, appear to be correct but jumbled. Chaim Goodman-Strauss of the Museum of Mathematics noted in an email that a paper describing a three-dimensional aperiodic tile has some novel mathematical ideas but is “unnecessarily difficult to read… I figure this is pretty representative across the corpus.” It is, he notes, not remotely close to being in publishable form according to traditional mathematical norms. Put another way, “The stuff I’m familiar with is gross to look at,” one topologist wrote on Twitter.

In some cases, bad writing crosses a line from obfuscating substantive ideas to, in the judgment of experts, simply not holding up. Mihalis Dafermos, a prominent expert in the math of black holes at Princeton University, said he couldn’t point to a specific flaw in several papers in his area of expertise, because the papers were too vaguely written to even approach the standard of proof that mathematicians expect. They’re essentially not even wrong. “In their current form at least, the papers are written in a very synoptic style and look far from constituting in of themselves a proof, let alone a proof that a person could verify,” he said.

Many mathematicians are exasperated. But certainly some are excited. “It’s clear that the OpenAI release includes major advances,” wrote Jeremy Avigad, the director of the Institute for Computer-Aided Reasoning in Mathematics, in an email. “We will learn a lot from the processes the mathematical community will develop to address the problem [of translating back and forth from Lean].” But perhaps the best that can be said of the papers at the moment is, as Daniel Litt of the University of Toronto suggests, that they be seen as “something like ‘research findings’ or ‘raw data’ at this point,” rather than as results in and of themselves. Which is, he notes, a “very unusual situation.”

In other news:

The Association for Human Mathematics, a group of over 800 mathematicians including Fields medalist Peter Scholze, issued a call to boycott OpenAI (which was then reposted by UCLA mathematician Terry Tao on his blog): “Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power.”

In response to the influence of AI on math, Thomas Bloom announced major changes to the structure of his website erdosproblems.com, which had been a hotbed of early AI-math results. The changes are intended to increase attention to why things are true rather than treating the Erdős problems as a scoreboard.

The technology firm OpenAI has announced the solutions to 377 open questions across nearly every mathematical subdiscipline.

The results are spread over 722 papers, which OpenAI has uploaded to the Github code repository. They were achieved by a new, unnamed internal model that the company intends to release publicly in the near future, once they deem it safe. All of the papers were written by this model; only one, on a zero-free region of the Riemann zeta function, was edited by a person.

The models seem to be growing more capable. Whereas OpenAI’s Navier-Stokes result in September used millions of dollars of computing power spread over a swarm of 10,000 intelligent agents, the computations behind the new results are, according to the firm, “very different in spirit to the Navier-Stokes setup.” With two exceptions — work on the Riemann zeta function and a proof of a particular case of the Hodge conjecture (both advances in pursuit of solutions to Millennium Prize problems) — each proof required only a nominal amount of computing time using the new model. “The average result used the equivalent of roughly 3 hours of ChatGPT Pro,” OpenAI wrote in a press release. That said, the new model failed on the vast majority of the roughly 4,000 problems it attempted to solve.

According to OpenAI, about half of the results have been formally verified in the programming language Lean. They do not expect any major obstacles to formalizing the remaining half, but rushed to share the results on the recommendation of an advisory group of mathematicians they recently convened. In the formal proofs obtained so far, no errors were discovered to have been made by the model, though in a handful, the formalization process revealed mistakes in the existing mathematical literature.

Mathematicians’ reactions to the announcement have been decidedly mixed. Some are expressing measured excitement. “350 is a lot, but time will pass and mathematicians will study the new content obtained here and see what use can be made of it (I am hopeful that the answer will be: a lot!),” Jordan Ellenberg of the University of Wisconsin wrote in an email. “There’s no hurry and it will all get done.”

According to Jeremy Avigad, who runs the Institute for Computer-Aided Reasoning in Mathematics at Carnegie Mellon University, “It’s against the spirit of mathematics to keep secrets, so I think it is generally a good idea for OpenAI to release their results.”

But other mathematicians are concerned about the implications of publishing such a massive trove of proofs that no person fully understands yet. In a series of Mastodon posts written prior to the release, Terence Tao of the University of California, Los Angeles noted that bulk-published proofs short-circuit the ways in which proofs have traditionally catalyzed the creation of knowledge. My colleague, Quanta’s math editor Jordana Cepelewicz, wrote about this phenomenon at length earlier this week. Tao is far from an AI opponent — as he points out, it’s possible to use AI in a way that preserves “all of the valuable followup activities that traditionally flow out of that solution. But at the current time, the opposite is often occurring… solutions to open problems are now being harvested at large scale in an unsustainable fashion, leaving entire fields of mathematics much less fertile than when such problems were solved in the traditional ‘Math 1.0’ fashion.”

For those inclined to anthropomorphize computer software, OpenAI’s anonymous new model today became one of the most prolific mathematicians in history. Seen in another light, as one anonymous online wag put it, “OpenAI Releases the Final Ten Minutes of 500 Previously Unreleased Films, Ushering in a New Era of Movie Watching.”

In other news:

A group of mathematicians announced the creation of Hexagon, a new repository for research in math and theoretical computer science.

The practice of mathematics is being remade by AI at a rate that’s often hard to fathom. Young mathematicians are facing those changes with grief, anger, and new ideas. As one doctoral student put it, the constant generation of new AI proofs that humans don’t yet understand “breaks our system. It just takes it to its absolute limit and destroys it.” As researchers work to change this system and save their field from potential extinction, will future generations be attracted to the new discipline that emerges? I reported on the anxious conversations taking place in math departments across the country in Quanta’s latest column: “Is AI the End of Math As We Know It?” —Jordana Cepelewicz