AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Single-fold Diophantine representations

Can the mathematical statement in Single-fold Diophantine representations be proved and verified machine-checked in Lean?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 242)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'Single-fold Diophantine representations'. Every recursively enumerable set of natural-number tuples has a polynomial Diophantine representation with exactly one complete auxiliary tuple for each member. This proves the single-fold conjecture and, consequently, the finite-fold conjecture.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 242). The Lean development was not rebuilt locally.