OpenAI's Math Proofs on GitHub: What the Lean Files Actually Show

TL;DR: OpenAI posted Lean formalizations of its math results to GitHub, which means some of these proofs can be machine-checked by anyone, and that is the part worth your attention, not the headline about “solving open problems.”

The primary source here is OpenAI’s post “Sharing AI progress in mathematics,” which announces new results on open problems from an internal frontier model and points to formalized Lean proofs and research details on GitHub (github.com/openai/math, with preprints under github.com/openai/math/tree/main/preprints). The thread surfaced on Hacker News the same day, mostly pointing back to those same repos. So the story is really two things glued together: a claim about capability, and a set of artifacts you can actually inspect. Those deserve to be judged separately.

What did OpenAI actually release?

Two categories of thing. One is prose: a blog post describing progress on open problems in mathematics attributed to an internal frontier model. The other is code: Lean proof formalizations and preprints checked into a public GitHub repo.

That split matters more than it looks. A blog post saying “our model solved hard math” is a claim. A Lean proof is a different animal. Lean is a proof assistant, which means a proof written in it either type-checks or it does not. If OpenAI formalized a result in Lean and the file compiles against a known axiom set, then the correctness of that specific argument is not a matter of trusting OpenAI. It is a matter of running the checker.

So the useful question is not “did OpenAI solve open problems.” It is “which of these results shipped with a Lean file that compiles, and against what.” Those are the ones where the burden of proof has actually moved off the press release and onto something reproducible. For anything that is prose-only or an informal preprint without a checked formalization, you are back to trusting a lab’s description of its own unreleased model. Treat those two tiers differently.

Why does Lean change the trust equation?

Most AI math claims over the last two years have been soft in a specific way. A model produces an argument, humans skim it, it looks plausible, headlines follow. The failure mode is that language models are very good at producing text that reads like a correct proof while containing a step that does not hold. Confident, fluent, wrong. The fluency is exactly what makes it dangerous to eyeball.

Lean removes the eyeballing. The proof assistant does not care how the argument reads. It cares whether each inference is justified. This is why formalization is the honest way to make a capability claim in math: it is self-checking by a party that cannot be charmed by good writing.

There is still fine print. A Lean proof is only as meaningful as the thing it claims to prove. The theorem statement at the top of the file is written by a human (or a model), and if that statement is subtly weaker than the “open problem” being advertised, the compiled proof is true but less impressive than the headline. So when you open these files, read the statement first, not the proof. Check that what got formalized is the thing that was hard. This is the step most readers will skip, and it is where the real scrutiny lives.

The other caveat: “internal frontier model.” The model that produced these is not one you can query. So even a verified proof tells you the proof is correct. It does not tell you how much human steering, retries, or scaffolding went into getting there, or whether the same system reproduces on the next problem. Verifiability of the output is not the same as reproducibility of the process.

How should a practitioner read this release?

Start with the repo, not the blog post. Go to github.com/openai/math, find the Lean files, and look at three things in order: the theorem statement, the axioms and imports it depends on, and whether the surrounding notes tell you it actually builds. If you have Lean installed, the strongest move available to any reader is to clone it and run the checker yourself. That is a rare thing to be able to say about an AI capability announcement, and it is the reason this one is more interesting than most.

For the preprints, apply normal preprint skepticism. A preprint is not peer-reviewed and not machine-checked unless it comes with a formalization. The value of OpenAI putting preprints next to Lean files is that you can see which claims graduated from “we wrote it up” to “we proved it to a machine.” Sort them that way in your head.

For everyone building products on reasoning models: the transferable lesson is the method, not the math. If you have a domain where correctness can be encoded in a checker, a type system, a test suite, a formal spec, a simulator, you can hold a model to a standard that does not depend on human review bandwidth. That is the actual frontier worth copying. Math has Lean. Code has compilers and tests. Finance has reconciliation. The pattern is: let the model generate, let a checker that cannot be fooled by fluent output decide.

Is this a breakthrough or a demo?

Both and neither, and the honest answer depends on the files. If the Lean formalizations cover results that mathematicians agree were genuinely open, and they compile, that is a real and specific advance, narrower than “AI does math” but more solid than almost any prior claim because it is checkable. If the formalized statements turn out to be reductions of the hard problems, or the impressive-sounding results are the prose-only ones, then the signal is mostly that OpenAI is getting serious about formalization as a credibility tool. Either outcome is informative.

What I will not do is call it before reading the statements, and neither should anyone else. The whole point of shipping Lean is that you no longer have to take the lab’s word for it. The worst way to respond to a verifiable artifact is to argue about it from the headline.

A builder’s move this week is small and concrete: clone github.com/openai/math, open two or three Lean files, and read the theorem statements before the proofs. You are not auditing OpenAI’s model. You are learning to tell a checked claim from an advertised one, which is a skill that will matter on every AI announcement from here forward. The catch most people will miss is that the Lean files raise the bar for OpenAI’s verified results and, by contrast, quietly lower your confidence in every unformalized claim sitting right next to them. Same repo, two very different levels of proof. Read them that way.