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

Proves the subcritical Hénon–Lane–Emden conjecture: for small enough powers, these equations have no positive solution.

1 paper September 24, 2026 Explained by AI

Some physics problems lead to two linked equations, where each unknown is driven by a power of the other. The Lane–Emden conjecture says that when the powers are small enough, no positive solution fills all of space. A weighted form adds powers of the distance from the origin. The paper settles both forms, with no extra assumption on symmetry or behaviour far away. A Lean statement covers the main theorem.

First step

—

Significance

Major

It settles the Lane–Emden conjecture for systems and its weighted form. Earlier proofs covered only low dimensions or added conditions.

Trust

Formal proof listed

Field

Partial differential equations

1 paper

The explanation

Start with one equation in three dimensions: −Δu = u⁵. Here Δ is the Laplacian, the sum of the second derivatives in each direction. It measures how much u at a point differs from its average nearby. The function u = (1 + r²/3)^(−1/2), where r is the distance from the origin, solves it. At r = 1, u = 0.866 and both sides equal 0.487. This solution is positive everywhere in space. Such a solution is called entire.

Now take two unknowns, u and v, with −Δu = v^p and −Δv = u^q. This is the Lane–Emden system. In dimension n the critical line is 1/(p+1) + 1/(q+1) = (n−2)/n. The example above sits exactly on it: n = 3 and p = q = 5 give 1/6 + 1/6 = 1/3. The conjecture says that strictly above this line, with smaller powers, no positive entire solution exists. For p = q = 4 in dimension 3, the left side is 0.4, which is above 1/3.

Gidas and Spruck proved the one-equation caseSource 1. Serrin and Zou proved the system in dimension 3 under a growth conditionSource 2. Later work removed that condition, and Souplet settled dimension 4Source 3. The weighted Hénon form multiplies the right sides by |x|^A and |x|^B. Li and Zhang proved its dimension-3 caseSource 4.

The paper claims the full answer in every dimension n ≥ 2Source 5. When (n+A)/(p+1) + (n+B)/(q+1) > n − 2, no positive entire solution exists. Setting A = B = 0 gives the Lane–Emden conjectureSource 6. No symmetry, boundedness or condition far from the origin is neededSource 7. Together with a known radial existence theorem, it settles Phan's Conjecture C in fullSource 8.

The weighted case is not a simple copy. Take dimension 5, with p = q = 4 and A = B = 3. The weighted test gives 8/5 + 8/5 = 3.2, above 3. The unweighted test gives 2/5, below 3/5Source 9. The obstacle is that shifting the solution sideways no longer gives a solution, because the weights depend on the originSource 10. The paper instead zooms in and out about the origin. A local energy identity and a pressure estimate on short intervals then give a bound that forces a contradictionSource 11.

How sure is this? Lean, a computer proof checker, has a formal statement of the main nonexistence theorem. So the paper proves it, as far as the Lean statement matches the paper. The critical equality case is not in the Lean scope. No specialist review of the paper is published.

What it doesn't show. This does not cover the critical case, where the inequality becomes an equality; there solutions can exist. It does not construct any solutions itself.

Where it came from

This result comes from an unreleased OpenAI model, published in the openai/math release on 6 October 2026.

Hype check

A major result with a Lean statement of the main theorem. It covers only the strict inequality; the critical case is outside it. No specialist review is published.

Words used

Laplacian (Δ): The sum of the second derivatives of a function in each direction; it compares a value with its nearby average.
Entire solution: A solution defined on all of space, not just a bounded region.
Lane–Emden system: The pair of equations −Δu = v^p and −Δv = u^q.
Hénon weight: A factor |x|^A, a power of the distance from the origin, that multiplies a right-hand side.
Critical line: The exact balance of powers, 1/(p+1) + 1/(q+1) = (n−2)/n, where solutions first appear.
Subcritical: Strictly on the side of the critical line with smaller powers.
Liouville theorem: A result saying that a solution on all of space must be trivial or cannot exist.

The original paper

The Subcritical Hénon–Lane–Emden Conjecture (PDF, opens in a new tab)
September 24, 2026 Formal proof listed

Lean notes

All quoted lines (11)

The scalar subcritical Liouville theorem of Gidas and Spruck is a starting point for this question.
The Subcritical Hénon–Lane–Emden Conjecture Back to text
Serrin and Zou proved the unweighted three-dimensional assertion under a growth condition; Pol\'a\vcik, Quittner, and Souplet removed that condition, and Souplet settled dimension four.
The Subcritical Hénon–Lane–Emden Conjecture Back to text
Serrin and Zou proved the unweighted three-dimensional assertion under a growth condition; Pol\'a\vcik, Quittner, and Souplet removed that condition, and Souplet settled dimension four.
The Subcritical Hénon–Lane–Emden Conjecture Back to text
Fazly and Ghoussoub obtained bounded and stability-based results for nonnegative weights; Li and Zhang subsequently proved the weighted conjecture in dimension three without a boundedness assumption.
The Subcritical Hénon–Lane–Emden Conjecture Back to text
We prove the subcritical H\'enon–Lane–Emden conjecture: for every dimension $n\ge2$ , 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)>n-2$ .
The Subcritical Hénon–Lane–Emden Conjecture Back to text
Theorem … resolves Huang and Zou's Conjecture B positively and yields Corollary … by setting $A=B=0$ .
The Subcritical Hénon–Lane–Emden Conjecture Back to text
No radial symmetry, boundedness, integrability, finite energy, stability, or growth or decay condition at infinity is required.
The Subcritical Hénon–Lane–Emden Conjecture Back to text
For $n\ge3$ and $A,B>-2$ , its nonexistence conclusion joins the radial existence theorem of Bidaut-V\'eron and Giacomini to prove Phan's Conjecture C in full, including existence on the critical hyperbola.
The Subcritical Hénon–Lane–Emden Conjecture Back to text
For instance, $n=5$ , $p=q=4$ , $A=B=3$ satisfies Equation (…), whereas $1/(p+1)+1/(q+1)=2/5<3/5$ .
The Subcritical Hénon–Lane–Emden Conjecture Back to text
Translations do not preserve the equation, and an endpoint of a layer $\{|x|^B u(x)^q>t\}$ has value $(t/|x|^B)^{1/q}$ , not the constant $t^{1/q}$ .
The Subcritical Hénon–Lane–Emden Conjecture Back to text
Here a localized potential-kernel virial identity and an energy-relative interval-pressure estimate supply that bound throughout the subcritical range.
The Subcritical Hénon–Lane–Emden Conjecture Back to text

Other sources

openai/math, Lean scope note for family 370 The formalized result proves nonexistence of positive entire solutions to the subcritical Hénon–Lane–Emden system.
openai/math release notes (2026): model provenance and review status manuscripts and supporting proof artifacts produced by an internal OpenAI model

369The hot spots conjecture for simply connected planar domainsPartial differential equations
366The planar Mumford–Shah regularity conjecture and local weak- L 4 gradient boundsPartial differential equations
375De Giorgi's conjecture in dimension eightPartial differential equations
349The Solomon–Yau least-volume conjectureDifferential geometry
344The metric Blaschke conjectureDifferential geometry

Browse Partial differential equations Named conjectures Lean-checked results