“Let me explain. No, there is too much. Let me sum up”

— Inigo Montoya in “The Princess Bride”

Here are some brief thoughts about the October 6th OpenAI release of 700+ math papers, a number of which contain claims of major breakthroughs. (The papers are organized somewhat better on this website.)

First of all, the release of these papers should have been coordinated much better. For example, I think that OpenAI should have released the Lean-formalized papers in one batch and the rest separately. Already a handful of (interrelated) non-Lean-certified papers in algebraic geometry, having to do with the Hodge conjecture, have been retracted due to an (apparently fatal) sign error. With the resources they have at their disposal, there is no reason for OpenAI to release things in such a sloppy manner. As of today, OpenAI says that 42% (300 out of 719) of their “top-line” results have been formalized in Lean.

OpenAI also ignored most of the suggestions from its Math+AI advisory group. This unfortunately doesn’t surprise me. The lack of care paid to the release of these papers, and the flaunting of math community norms in doing so, is one more warning sign that OpenAI has an unhealthy corporate culture. Unfortunately, the implications of this go far beyond mathematics. I don’t want to get into a long discussion of AI safety here, but there are many red flags (including but by no means limited to the infamous Hugging Face incident) which suggest that OpenAI is not taking safety concerns seriously enough. For more information, I recommend reading or listening to Ezra Klein’s recent interviews with David Robinson, Bill Gates, and Helen Toner, along with this essay.

Having said all of that, I’m surprised that many in the math community appear to be so skeptical of Lean proofs. Kevin Buzzard, who has arguably done more than anyone to popularize the use of Lean among mathematicians, recently wrote on his blog:

My own area (the Langlands philosophy) is full of arguments which seem to be “known to the experts” without a publicly-available write-up, and this situation was what caused me to become disillusioned with the field and ultimately withdraw from curiosity-driven research completely and switch to mathematical formalization. You cannot fool Lean; one learns this very early on. Lean will not accept proof by authority or proof by intimidation; it doesn’t work like that.

However, in contrast to the confidence Kevin and many other experts have in Lean, I’m seeing a ton of skepticism on social media, and I’ve also heard it in person. The reasons my mathematician friends give for their skepticism range from “I don’t trust anything that was touched by AI” to more focused remarks like “I read somewhere that the statement of the Riemann hypothesis in Lean’s math lib was wrong for some period.”Another person wrote, “There seem to be some technical reasons to consider this a harder problem than is acknowledged, see e.g. the paper Navier-Stokes lost in translation.

My response to the latter comment was as follows:

Let’s be precise here. I completely agree with the main thesis of the paper you linked to, and I’ve been saying the same thing to colleagues for a while now. But it’s a different issue than what I thought we were talking about here. If OpenAI says that they’ve formalized Theorem X in Lean, it doesn’t mean the accompanying LaTeX write-up gives a fully correct proof; in fact, that proof could have major gaps. It does mean that either (a) The theorem is correct and OpenAI did come up with a proof; (b) the Lean proof is certifying a different statement from what’s intended; or (c) the Lean proof is wrong but it compiled correctly due to a bug in the Lean kernel. What I’m saying is that I consider (b) and (c) possible but rather unlikely. I don’t know how to attach a precise likelihood to either (b) or (c), but my personal estimate would be less than 1%. So my default assumption is (a). If this is proved wrong, it would be very interesting and I will certainly update my Bayesian priors accordingly.

I would be happy to hear arguments from people knowledgeable about Lean if they think that I’m underestimating the likelihood of (b) or (c), or if I’m missing an additional option (d) (e.g. I suppose OpenAI could just be faking the existence of a Lean certificate, hoping that no one bothers to check). The thing is, I haven’t seen a single example of a theorem that was both deemed correct by a (recent) frontier-level AI model and certified as true in Lean which later turned out to be false. Whereas I know plenty of examples of theorems that a human said was correct which later turned out to be false. The only examples I know of Lean proofs that turned out to be wrong are things like the Collatz conjecture incident, which as I understand it was engineered specifically to highlight a bug that had been found in the Lean kernel. I think (b) is certainly an issue, but in my experience frontier LLMs are very good at this sort of thing now, and I’m confident that mathematicians who understand both Lean and the statements of the theorems being claimed will quickly find any mismatch between natural language statements and the corresponding Lean versions. I do think (c) is theoretically possible, and that one or more of the Lean formalizations is a Hugging Face-style hack of the Lean kernel, but I don’t view this as particularly plausible. [Note added in post: see Kevin Buzzard’s comments on (b) and (c) below; he is signed in as ‘xenaproject’.]

Anyway, subject to all the above caveats, the mathematical results being claimed by Open AI are quite breathtaking, and despite how irritating OpenAI’s cavalier attitude has been, this appears to mark a watershed moment in the history of mathematics. Among the Lean-formalized results, we have for example:

Ten OpenAI results formalized in Lean 4

The following ten results have been released by OpenAI with Lean 4 formalizations. (Formalization status was checked on October 8, 2026.)

Item	Result	Family
1	Quasi-Riemann hypothesis and uniform exclusion of Landau–Siegel zeros	#003
2	Matrix multiplication with exponent at most 9/4	#107
3	A torsion-free hyperbolic group that is not residually finite	#252
4	Exact discrete Fourier transforms below n log n	#130
5	Erdős–Turán reciprocal-sum conjecture	#159
6	Ordinary two-point Chowla conjecture	#007
7	Cannon’s conjecture	#246
8	Counterexamples to Hadwiger’s conjecture	#157
9	A counterexample to Sidorenko’s conjecture	#161
10	Derandomization of logarithmic space: L = RL = BPL	#103

It seems to be widely agreed that the most spectacular of these results is the Quasi-Riemann hypothesis. For example, Alex Kontorovich recently posted the following to X:

“Quasi-RH?!?!???! Are you kidding me? If a human did this, it would be an instant Fields Medal, no questions asked. … I thought maybe they’d fatten that up a bit, that’d be a massive breakthrough. But no. They got a zero free strip!!!! Insane”

(Note of caution: one of my colleagues recently wrote that OpenAI ‘almost solved the Riemann Hypothesis, to which I responded: “I wouldn’t characterize it as ‘almost solving’ the Riemann Hypothesis. It’s quite possible that an entirely different approach will be needed to prove RH (presumably they tried rather hard to push this method further!). No need for hyperbole when the verifiable reality is already so jaw-dropping.”)

Aside from implying “No Siegel Zeroes”, a result which has vexed the number theory community for nearly 100 years, Quasi-RH also gives the first unconditional polynomial time algorithm for finding square roots modulo a prime number, which is something people have also thought about for at least 100 years and which was an open problem I would always tell students about in my undergraduate number theory course at Georgia Tech. (I also blogged about this problem here.)

About the Erdös-Turán conjecture, my colleague Ernie Croot wrote:

The Erdos-Turan result is one that Tim Gowers, Terry Tao, Ben Green, E. Szemeredi, and a whole generation of people have worked on. Gowers and Tao had developed whole theories about how to attack problems of quantitative bounds on largest sets A of [N] without k-APs. When M. Sawhney came to give a talk on the latest bounds a year ago, I asked him how close they were to solving the problem (I asked in different, but equivalent way), and what I got back was that he thought their approach wouldn’t come even close to cracking it. Now not only did OpenAI’s model crack it, but it even produced what are called “Behrend-type bounds”, which is just absolutely insane, as it’s essentially optimal (well, up to fussing about a certain exponential parameter). It’s like the holy grail of the field (additive combinatorics), brushing aside all prior work.

Finally, let me conclude this post on a more human note. A former Ph.D. student emailed me the following yesterday:

Do you think there is still room for human mathematicians in the future? 

If the answer to the previous question is yes, what can I possibly do to make a positive contribution to it? 

I think this is the central question that we mathematicians should be focusing on right now. But I don’t have space in the margins of this blog post to write a reasonable answer. So I will instead refer readers to this previous blog post of mine and this thoughtful article by Jordana Cepelewicz of Quanta Magazine, which gives a reasonable approximation to my own views. In particular, here is a quote from the end of Jordana’s piece:

It will be hard. Inertia is powerful. But mathematics could come out of this stronger than before. Forced to name and prioritize what people love and value about the field, current and future mathematicians can emphasize skills that have previously been deprioritized: the ability to communicate and share knowledge, to develop a broad vision, to experiment with original ideas without feeling the need to publish theorem after theorem. To think deeply.

“I think there is a good future where we come out way ahead of where we are now, where we learn a huge amount of interesting math,” Litt said. “We have people doing the coolest stuff they’ve ever done. We have a really vibrant community of people who deeply understand stuff.”

If we can’t adapt, he added, “whose fault is that?”.

AI disclosure note: I used ChatGPT to create the table “Ten OpenAI results formalized in Lean 4”.