The Lane–Emden conjecture
From OpenAI Aftermath
The Lane–Emden conjecture asserts that the system −Δu = vp, −Δv = uq has no positive solution on ℝn whenever 1/(p + 1) + 1/(q + 1) > (n − 2)/n, that is, below the critical Sobolev hyperbola. Its weighted form, the Hénon–Lane–Emden conjecture, concerns −Δu = |x|Avp, −Δv = |x|Buq. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof of the subcritical weighted assertion in every dimension, with a Lean formalization of the main theorem. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introduction of the manuscript:
- The scalar subcritical Liouville theorem of Gidas and Spruck is the starting point. For systems, Mitidieri developed a Rellich identity and early nonexistence regions; Serrin and Zou proved the unweighted three-dimensional case under a growth condition, which Poláčik, Quittner and Souplet removed, and Souplet settled dimension four. Li, Li and Wei obtained a further unweighted region for p, q ≥ 1 in every dimension n ≥ 5.
- Liouville theorems of this kind also serve as inputs to rescaling arguments for a priori bounds and singularity estimates.
- For the weighted system, Bidaut-Véron and Giacomini identified the critical hyperbola in the radial theory. Phan formulated the weighted question for A, B > −2 as a conjecture and proved bounded, low-dimensional and conditional cases; Fazly and Ghoussoub, Li and Zhang (dimension three) and Li (restricted ranges in dimensions four and five) obtained further cases, and Huang and Zou stated the all-real-weight, origin-continuous assertion as a conjecture.
The original result
- Claim. Theorem 1.1 of The Subcritical Hénon–Lane–Emden Conjecture states that for every integer n ≥ 2, all p, q > 0 and all real A, B with (n + A)/(p + 1) + (n + B)/(q + 1) > n − 2, there are no positive functions u, v, continuous on ℝn and twice continuously differentiable away from the origin, satisfying the weighted system away from the origin. No radial symmetry, boundedness, integrability, finite energy, stability, or growth or decay condition at infinity is assumed. Corollary 1.2 is the unweighted Lane–Emden conjecture for n ≥ 3; combined with the radial existence theorem of Bidaut-Véron and Giacomini, the manuscript also records the resulting existence–nonexistence classification for A, B > −2.
- Method, as described: origin-centered dilations give uniform source masses on a fixed ball; a compactly supported virial identity built from the potential kernel retains the weight coefficients; and an interval comparison along directions in a small cap around the radial direction, with intervalwise weights, bounds a localized energy, which subcritical scaling then contradicts.
- Sources. The manuscript The Subcritical Hénon–Lane–Emden Conjecture at commit
1581d4c. - Formalization, as described by the repository. The scope note states that the formalized result proves the nonexistence statement of Theorem 1.1, including the globally twice-differentiable unweighted case for n ≥ 3, and that the critical equality case is not included. The Comparator statement is
HenonEmden.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 21 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | L. Mei, J. Wei, A proof of the fractional Lane–Emden conjecture (arXiv:2610.10188) | Extension (fractional) | For 0 < s < 1 and p, q > 0, the system obtained by replacing −Δ with the fractional Laplacian of order 2s has no strictly positive entire solution when 1/(p + 1) + 1/(q + 1) > (n − 2s)/n, with no symmetry, boundedness, energy or decay assumption. The authors state that the proof adapts the manuscript's localized potential-kernel virial and source-layer interval-pressure method to the Riesz kernel. | arXiv preprint. |
| 2026-10-08 | MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statement) | Rates the family "full": the Lean theorem states the weighted nonexistence assertion with the manuscript's hypotheses and no symmetry or growth assumption; the radial existence criterion is background and not stated. Records a sandboxed Comparator pass for HenonEmden. |
MathVet states that it does not claim any theorem false and reports what was machine-checked as stated. |
| 2026-10-08 | atimics/math2, Cross-family corollaries of openai/math, entry GE-8 (GitHub, commit 2c0f005) |
Use (Lean specialization) | Records, as a Lean-checked implication from the collection's formal statement, the scalar case: for n ≥ 2, p > 0 and n − 2 < 2(n + A)/(p + 1), there is no positive u with −Δu = |x|Aup on ℝn minus the origin. | The catalogue labels each entry by its form of support and states that the entries are conditional on OpenAI's claims. |
| 2026-10-10 | cert-machine, openai/math lane K: run 38019899278 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the HenonEmden solution, in 803 s. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, memory, errors) does not list HenonEmden, so it was accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-13 | mingfeng87/Lane-Emden-type-conjecture (GitHub, commit 3069a73) |
Extension (fractional and polyharmonic, weighted; drafts) | Two manuscripts extend the localized kernel virial and interval pressure method, citing the OpenAI manuscript: Liouville theorems for weighted fractional Lane–Emden systems with all real weights and all positive powers, and for weighted polyharmonic systems of order 2m with p, q ≥ 1, pq > 1 under (N + A)/(p + 1) + (N + B)/(q + 1) > N − 2m. | The README marks both documents as drafts, "candidate proofs, not yet fully verified", obtained "through extensive dialogue-based training with AI" and under verification by the team. |
| 2026-10-16 | K. Li, H. Lu, Z. Zhang, The fractional Hénon–Lane–Emden conjecture and some critical nonexistence phenomena (arXiv:2610.22802) | Extension (fractional, weighted) | Refines the method of the OpenAI manuscript and of Mei and Wei and extends it to fractional orders 0 < s < 1, proving subcritical nonexistence of positive classical solutions; gives examples with 0 < s < 1/2 and fixed nonzero weights where existence and nonexistence occur at different points of the same critical hyperbola. | arXiv preprint. The acknowledgements state that AI assistance was used in parts of the proof of the subcritical fractional conjecture. |
| 2026-10-20 | Y. Guo, Y. Hu, S. Peng, T. Yuan, arXiv:2610.27875, Classification of positive solutions to the critical Lane–Emden system | Extension (critical hyperbola) | For N ≥ 3 and (p, q) on the critical hyperbola, every positive classical solution is a translate and dilate of the radial ground state, without boundedness, decay or finite-energy assumptions. The authors base the radial-symmetry step on the manuscript's source-layer interval comparison, keeping its nonnegative midpoint term as a defect that measures the failure of radial symmetry. | arXiv preprint. The authors' declaration states that ChatGPT was used to explore research ideas and possible proof strategies and to improve the language of the introduction, and that all arguments were checked by the authors. |
Notes
- The earlier results are due to the authors named in the Background section, as recounted by the manuscript.
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.
