No. 03 · The observatory
Famous but irrelevant
The release’s most famous results thrill mathematicians. None changes a product, cost line or business decision.
- Status
- Open
- Families
- 003, 002, 006, 004, 017, 032, 087, 196, 197, 287, 294, 376
- Verification
- Mixed. 003, 017, 087 and 287 are Lean-checked. 002, 004 and 032 are not.
- Time to market
- None. No business pathway.
- What to do
- Nothing, commercially
Why doesn’t fame mean business value?
Ignore headline fame when you judge business value. Ask which buyer’s tool changes.
Fame and business value measure different things.
Fame measures how long experts have tried a question. It also tracks how central the question is inside mathematics. Business value needs a buyer whose tool changes.
Fermat’s Last Theorem and the Poincaré conjecture followed the same pattern. Both made history. Neither moved a product.
Across the release, 40 of 372 families have any business pathway. The famous results are not among them.
OpenAI posed about 4,000 problems and kept 372 results
Problems posed, result families kept, and families with a full Lean check. Snapshot 7 Oct 2026.
- Problems posed
- Families kept
- Fully Lean-checked
How to readEach bar is one stage. Longer bars mean more items.
NoteOpenAI never defined its significance filter or published failure counts.
Sourceopenai/math README and lean/formalization.yaml, commit fd4aeeb
What do the headline results prove?
Keep your products, security choices and roadmaps as they are.
The biggest result is the quasi-Riemann hypothesis, family 003.
The zeta function and all Dirichlet L-functions have no zeros past a boundary. That boundary sits at real part 7/8. The full Riemann hypothesis would push it down to 1/2. So this is a weaker, unconditional cousin.
Its 7/8 paper carries a Lean check. The 11/12 alternate proof does not.
The rest of the famous set:
- Hodge conjecture for CM abelian varieties (032): holds for one special class of shapes. No tool depends on it.
- Birch and Swinnerton-Dyer (002, 006). Proves much of the formula, for certain elliptic curves and almost all quadratic twists.
- Hilbert’s tenth problem over the rationals (004). No algorithm can decide every polynomial equation in fractions. No vendor needs one.
- Irrationality exponent of pi (017): pi resists close fractions. Computing or using pi stays the same.
- Kaplansky conjectures (196, 197, 294): groups that disprove three of them. They concern infinite algebraic objects.
- Free group factors (287): three operator algebras turn out to be the same. No applied consumer exists.
- Mahler conjectures (087): specific polytopes minimise a volume product. No business effect.
- Forced Navier-Stokes flows (376): forced fluid flows can carry out any computation. Fluid simulation software stays the same.
Does any of this touch encryption?
Keep your security plans unchanged. These results leave deployed encryption alone.
No. Encryption does not rest on these questions.
RSA and elliptic-curve encryption do not rely on the Riemann hypothesis. Some deterministic primality tests no longer need to assume it. Practice already uses fast randomised tests instead.
Elliptic-curve cryptography uses curves over finite fields. It does not depend on the Birch and Swinnerton-Dyer formula. Nothing in the 372 families weakens deployed cryptography.
How solid are the proofs?
Wait for expert peer review before calling any of these settled.
Verification varies widely across the famous set.
An independent GitHub user rebuilt the quasi-Riemann Lean proof on 2026-10-07. They reported 2,924 modules with zero errors. They also stated it “is not a substitute for expert peer review.”
About half the result families carry a full machine check
All 372 families by Lean status. Snapshot 7 Oct 2026.
- Fully Lean-checked
- Partly checked
- Not checked
How to readEach square is one family.
NoteA Lean check proves the formal statement. It does not prove the statement matches the paper.
Sourceopenai/math lean/formalization.yaml and history.md, commit fd4aeeb
What do experts say, and what should we do?
Read the praise as a signal about AI research capability. Revisit only if a standard changes.
Mathematicians are stunned by several of these results.
- Ben Green on quasi-RH: “absolutely shocking to me”.
- Álvaro Lozano-Robledo: “quasi-RH is huge! But it is not RH”.
- Vadim Alekseev on free group factors: “really impressed”.
- Michael Chapman names the Kaplansky refutations among problems he “grew up on”.
Lozano-Robledo also notes OpenAI aimed at the full Hodge and BSD conjectures. These are partial cases. He says the Hilbert result “would represent huge contributions”.
One researcher had “tried hard for a number of years” to prove the opposite. A tracker lists its Lean proof as “not yet reviewed”. We found no reception for the pi, Mahler or fluid results.
Commercially, these famous results need no action. They show what AI can now do in research. Revisit only if someone ties one to a named algorithm or standard.
The theorems are the exhaust; the engine behind them already makes money. Google’s AlphaEvolve, a similar AI search engine, recovers 0.7% of Google’s worldwide compute. That engine already works on companies’ own problems, where a machine can score answers.