The Lane–Emden and Hénon–Lane–Emden conjectures

Resolves the subcritical Lane–Emden conjecture and its weighted Hénon extension. For n ≥ 2, p,q\gt 0 and real A, B, the system -\Delta u=|x|^A v^p, -\Delta v=|x|^B u^q has no positive entire solution when (n+A)/(p+1)+(n+B)/(q+1)\gt n-2, with solutions continuous at the origin and classical elsewhere. No symmetry or growth assumption is needed. Known radial existence gives the exact existence criterion for n ≥ 3 and A,B\gt -2. (Lean)

Manuscript

The Subcritical Hénon–Lane–Emden Conjecture

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:The-Subcritical-Henon-Lane-Emden-Conjecture-September-24-2026}

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.

Result 370 · Partial differential equations. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.