AI Cracks the Quasi-Riemann Hypothesis? A Mathematician's Account of a Stunning Moment

When AI Starts Proving Mathematical Conjectures

On Lex Fridman's podcast, number theorist Alex shared a moment he still finds hard to believe: he personally witnessed the proof of the quasi-Riemann hypothesis being completed by an AI system. This expert, who has studied the Riemann hypothesis for years, admitted that he never thought he would see this day in his lifetime.

When the news was released, Alex was attending a dinner at the National Museum of Mathematics in New York. With a whiskey in one hand, he kept refreshing his phone—because he knew the paper would be released around 6 PM Eastern Time. When the words "quasi RH" appeared on the screen, his first reaction was confusion: "What do you mean? The quasi-Riemann hypothesis? For which function?" It wasn't until he confirmed that it involved the Zeta function and all Dirichlet L-functions, and that it had solved the no Siegel zeros problem, that he realized he might be witnessing a historic breakthrough.

"That far exceeded the boundaries of what I believed possible," he described his feelings at the time.

Understanding the Riemann Hypothesis in One Minute

For readers unfamiliar with number theory, Alex gave a minimalist explanation. The distribution of primes has always been a core problem in mathematics, and Riemann discovered that a function taking complex numbers as input and output—the Riemann zeta function—somehow governs the behavior of primes. The locations of the zeta function's zeros, that is, the complex inputs that make the output zero, determine how primes are distributed.

What makes this discovery so astonishing is that it connects the discrete, indivisible primes with the continuous complex plane. Alex used signal processing as an analogy: just as a microphone performs Fourier analysis on sound waves to convert them into amplitude and frequency, and a speaker then reconstructs the human voice, the zeta function does the same kind of signal processing analysis on primes. The frequency and amplitude information of the zeros can precisely recover the distribution of primes.

And what the Riemann hypothesis predicts is: all "Riemann waves" have exactly the same amplitude—like an orchestra playing the music of the primes, where every instrument sounds at exactly the same volume.

What is a Dirichlet L-function? The Riemann zeta function describes only the overall distribution of all primes, while the Dirichlet L-function is its generalization: given a modulus q, the L-function "sees" only primes in a certain residue class modulo q. For example, to study whether primes of the form 4k+1 and 4k+3 each account for half, one needs the Dirichlet L-function modulo 4. Each L-function has its own zeros, and the generalized Riemann hypothesis (GRH) asserts that these zeros also all lie on the critical line. The proof of the quasi-Riemann hypothesis covers the Zeta function and all Dirichlet L-functions, meaning it handles at once the deep regularities of prime distribution in arbitrary arithmetic progressions, with an impact far greater than a result concerning only a single zeta function.

What is a Siegel zero? A Siegel zero (also called a Landau-Siegel zero) refers to a possible anomalous zero of a Dirichlet L-function near the critical line on the real axis. If such a zero exists, it would severely disrupt the uniform distribution of primes in arithmetic progressions, leading to the famous "prime bias" phenomenon. For decades mathematicians have hoped to rule out the existence of Siegel zeros but have never been able to do so. The resolution of the "no Siegel zeros" problem that Alex mentioned is precisely one of the most significant parts of the quasi-Riemann hypothesis proof, because it directly concerns the controllability of prime distribution in the worst case.

Three Cognitive Upheavals in One Month

The proof of the quasi-Riemann hypothesis was not an isolated event. Alex revealed that this was already the third time in one month that he had been stunned by AI's capabilities.

The first was the formalization of Fermat's Last Theorem. He had given a talk in the Princeton mathematics department, explaining in detail the current state of Lean and mathlib, and judged that AI systems could at present only build one or two layers on top of existing libraries, being good at "jerry-rigging"-style patching but bad at what he called "canonization"—that is, refactoring rough code and placing it into its canonical position in the library. He was certain at the time that it would be at least three years before AI could formalize Fermat's Last Theorem.

As it turned out, the talk was on a Wednesday, and on Friday 13 million lines of Lean code appeared, with a sorry-free (i.e., complete and gap-free) formal proof generated by Anthropic's AI system. "Every single thing I said was proven wrong," Alex said.

The second was progress on the Navier-Stokes equations, and the third was the quasi-Riemann hypothesis.

Lean, mathlib, and "sorry" Lean is an interactive theorem prover that writes mathematical proofs as code that a computer can check line by line. mathlib is a mathematics library built on Lean, gathering tens of thousands of already-formalized definitions and theorems, and is the shared infrastructure of formalized mathematics. In Lean, sorry is a placeholder meaning "the proof here is skipped." A proof containing sorry merely states a conclusion without truly verifying it; a so-called "sorry-free proof" means every line of reasoning has been fully checked by machine, with no unproven gaps in between. Therefore, the 13 million lines of sorry-free code are astonishing because they represent a machine-verifiable proof of Fermat's Last Theorem, not merely a plausible-looking draft.

Formalization and canonization Alex distinguished two kinds of work: one is "jerry-rigging," that is, forcing a proof through with hastily patched-together code; the other is "canonization," that is, refactoring rough code and placing it into mathlib's canonical system and naming conventions. The former only seeks to make things run; the latter makes code reusable, maintainable, and dependable for subsequent proofs. AI is currently good at the former, while the latter still requires a great deal of manual refactoring, which is the technical meaning behind Alex's emphasis that "there is still a lot of work before mathlib quality."

Not an Elegant Proof, but Highly Significant

Alex particularly emphasized that the AI-generated proof still requires a great deal of work before reaching "mathlib quality." It is not a clean proof, full of jerry-rigging, and needs extensive refactoring and normalization. But he distinguished two levels of the problem: if the goal is to obtain a sorry-free formal proof, then the problem of autoformalization is basically solved.

As for the number of participants, according to Alex's understanding only two or three humans were involved, and their main work was "keep going"-style encouragement, with no domain expertise involved. He also cautiously pointed out that from the company's perspective there is an incentive to package the process as "breakthrough from a single prompt," but what groundwork and unstated steps may have been involved in the actual training is unknown to the outside world.

Scientists Can Be Wrong Too

In the face of such rapid progress, Alex maintained a scientist's candor: "Of everything I say today, 40% to 80% will be proven wrong in five years." He believes this is precisely the value of human discussion—through disagreement, deliberation, and the clash of discourse, the scientific process itself advances through trial and error, except that this cycle used to be ten years or a hundred years, and now it has been compressed to a few months.

He described the feeling as like "mourning": his own empirical model, built up over years, of the boundaries of AI capability had been completely shattered, "it does X and I believe it, it does 10X and I don't, but this time it was a million X."

One-line Summary

AI made successive breakthroughs in number theory, completing a proof of the quasi-Riemann hypothesis and formalizing Fermat's Last Theorem, far exceeding expert expectations.

Paragraph Summary

The article records number theorist Alex recounting on a podcast three times in one month that he was stunned by AI: an AI system completed the proof of the quasi-Riemann hypothesis, involving the Zeta function and all Dirichlet L-functions, and solved the Siegel zero problem; previously it had also generated 13 million lines of sorry-free Lean code, formalizing Fermat's Last Theorem. Alex used a signal-processing analogy to explain the Riemann hypothesis, noting that although the AI proof is inelegant and requires substantial refactoring, the problem of autoformalization is basically solved. Only two or three humans participated and no domain expertise was involved, and he cautioned that companies may not disclose the training groundwork. Faced with the collapse of capability boundaries, Alex candidly stated as a scientist that most of what is said today will be disproven in five years, and that science advances through trial and error, only now the cycle has been compressed to a few months.