# OpenAI's Ten Mathematical Results Tested Through Lean Certificates

DevFeed: [OpenAI's Ten Mathematical Results Tested Through Lean Certificates](<https://devfeed.tech/articles/who-writes-the-question-40146.md>)

Original publisher: [Read original article](<https://korbonits.com/blog/2026-08-01-who-writes-the-question/>)

Published: 2026-08-01T00:00:00Z

Content type: article

Language: en

Sources: [Alex Korbonits](<https://devfeed.tech/sources/alex-korbonits.md>)

Topics: [Lean](<https://devfeed.tech/topics/lean.md>), [OpenAI](<https://devfeed.tech/topics/openai.md>), [certificates](<https://devfeed.tech/topics/certificates.md>), [trust](<https://devfeed.tech/topics/trust.md>), [Artificial Intelligence](<https://devfeed.tech/topics/ai.md>)

Tags: [ai](<https://devfeed.tech/tags/ai.md>), [certificates](<https://devfeed.tech/tags/certificates.md>), [openai](<https://devfeed.tech/tags/openai.md>), [paper](<https://devfeed.tech/tags/paper.md>), [trust](<https://devfeed.tech/tags/trust.md>)

## AI overview

The article examines OpenAI's release of ten results on long-standing mathematical problems and reports independently building and checking the accompanying Lean certificates. It says all 38 headline theorems passed with no errors or non-standard axioms, while raising concerns about trusting definitions written by the same system that produced the proofs.

## Source excerpt

OpenAI shipped ten open problems with Lean certificates. I built all 550,000 lines and checked what they rest on. Everything passed -- and the only thing left to trust is 1,700 lines of definitions written by the same system that wrote the proofs.