No solutions below the curve?

The claim, in plain words

Over a century ago, Lane and Emden modelled a star as a ball of gas held together by its own gravity, which leads to the equation minus the Laplacian of u equals u to the power p. In three dimensions our computer finds the star’s edge, where u first reaches zero: at pi for p equal to one, about 6.9 for three, about fifteen for four, and never for five. Five is the critical exponent: Gidas and Spruck proved in 1981 that below it, no positive solution fills all of space.

For two coupled equations, minus the Laplacian of u equals v to the p, and minus the Laplacian of v equals u to the q, the boundary becomes a curve, the critical hyperbola, and the Lane-Emden conjecture says no positive solution fills space below it. Our computer shoots radial solutions in three dimensions with p equal to three: below the curve even the best-tuned one dies; on and above it, one tuned solution survives. The conjecture was known for radial solutions, in dimension three and in dimension four, and in parts of higher dimensions; in five dimensions, a thin band next to the curve, with unequal powers, was still not covered by the earlier results we checked. With weights, a power of the distance to the origin, it is the Hénon-Lane-Emden conjecture, proved only in dimension three. A December 2025 paper still called even the unweighted conjecture open in higher dimensions.

Result 370 is one OpenAI paper, 20 pages, dated September 24 and made public October 6, 2026. It claims that in every dimension from two up, for all positive powers and all real weights, whenever the pair lies below the weighted critical curve, the system has no strictly positive solution on all of space, continuous at the origin and classical elsewhere. No symmetry, boundedness or decay is assumed. The unweighted Lane-Emden conjecture is a special case.

What it doesn’t claim

Not claimed: anything new on the critical curve or above it. Above the curve, and on it, radial solutions were already known to exist, by Bidaut-Véron and Giacomini, so with that known result the paper gets an exact existence criterion in dimension three and up, for weights above minus two. Some cases, dimension two or small powers, are elementary.

Where it stands

Posted as a preprint

OpenAI, 20 pages, dated September 24, 2026

Peer reviewed

Not yet; no specialist verdict

Formalized in Lean

The main theorem, with no extra hypotheses, and the unweighted case (scope notes)

Last checked October 19, 2026. The paper is unrefereed and unchanged since release. Its main theorem has a Lean proof, about 12,700 lines, not run by us, which also covers the unweighted case. Two follow-up preprints, on October 7 and 16, build on its method for fractional versions; they use it, but they are not reviews. We found no specialist verdict. OSVerify has not reviewed it.

How the proof goes

1. Scaling versus a uniform bound. First, solutions are exactly potentials: u is the gravitational potential of a source built from v, and v of one built from u. Then a scaling argument: zooming out around the origin turns a solution into another solution whose local energy is at least the old one times a power of the zoom, and below the curve that power is positive, so these zoomed solutions would have energy growing without bound. Near the curve the power is tiny: at one of our sample points in five dimensions it is about 0.09, and a millionfold zoom guarantees a factor of only about three and a half. So the paper proves the opposite: a single energy bound that holds for every solution.
2. Three ingredients. The bound comes from three ingredients: a localized virial identity, a one-dimensional lemma about intervals on two parallel lines, and a pressure estimate from level sets sliced along nearly radial directions. Our computer checks the interval lemma on 120 random cases with no violations. Every error term has the form of a small multiple of the energy plus a constant, so it can be absorbed, and the bound plus the scaling growth gives the contradiction.

The numbers in the video

• Ours: in 3-D the Lane–Emden star's edge is at π for p = 1, about 6.9 for p = 3, about 15 for p = 4, and never for p = 5.
• Ours: for the system with p = 3 in 3-D, the best-tuned radial orbit dies below the curve (q = 5, 7, 9) and stays positive on and above it (q = 11, 13, 15).
• Ours: at n = 5, p = 1.55, q = 3.65 the scaling exponent is about 0.09, so a millionfold zoom guarantees a factor of only about 3.55.
• Lean: 96 files and 12,709 lines in the import closure of the comparator's solution (counted by us; not run by us).

Read the source

• The Subcritical Hénon–Lane–Emden Conjecture (PDF), 20 pages.
• The Lean formalization notes.
• The collection’s catalog, where this is result 370.

The paper

OpenAI groups related papers into one result; this one has a single paper.

• The Subcritical Hénon–Lane–Emden Conjecture

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.