AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

Petty’s projection-volume conjecture in dimensions at least four

Can the mathematical statement in Petty’s projection-volume conjecture in dimensions at least four 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 088)

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 'Petty’s projection-volume conjecture in dimensions at least four'. We prove that ellipsoids uniquely minimize the volume of the projection body among convex bodies of fixed volume in every dimension at least four. This proves Petty's projection-volume conjecture in these dimensions.

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