Lean formalization in OpenAI math repository (Result 370)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of 'The Subcritical Hénon–Lane–Emden Conjecture'. We prove the subcritical Hénon–Lane–Emden conjecture: for every dimension n ≥ 2, positive powers p, q, and real weights A, B, the system has no strictly positive entire solution when (n+A)/(p+1)+(n+B)/(q+1)\gt n-2. Solutions need only be continuous at the origin and classical elsewhere, without a condition at infinity. For n ≥ 3 and A,B\gt -2, combining this result with the radial existence theorem of Bidaut-Véron and Giacomini proves Phan's Conjecture C in full: a positive radial entire solution exists whenever the strict inequality fails.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 370). The Lean development was not rebuilt locally.