OpenAI's release included Lean 4 formalizations of the results in the openai/ten-proofs repository, a paper describing the solutions, and an LLM-generated PDF reconstructing how each proof came together from the unpublished reasoning traces — a decent level of transparency, though the prompts themselves were not published.

On transparency: the openai/ten-proofs repository holds Lean 4 formalizations, backed by a paper and an LLM-generated PDF that reconstructs the proof process from reasoning traces — decent disclosure, though the author still wants the prompts themselves released. ✦ AI generated

Article author (via Hacker News) · Simon Willison's Weblog · 2026-08-01 · original ↗

The openai/ten-proofs repository has Lean 4 formalizations of their results, and there's also a paper describing the solutions and an additional LLM-generated PDF where the model "reconstructs how the proof came together" based on the unpublished reasoning traces. That's a decent level of transparency, but I want to see the prompts they used!

Read full article ↗excerpt · fair-use quotation