Aftermath bot: New page: the Lane–Emden conjecture, from public sources; Main link

2026-10-21T02:33:36Z

New page: the Lane–Emden conjecture, from public sources; Main link

New page

The '''Lane–Emden conjecture''' asserts that the system −Δ''u'' = ''v''''p'', −Δ''v'' = ''u''''q'' 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''|''A''''v''''p'', −Δ''v'' = |''x''|''B''''u''''q''. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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 [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/The-Subcritical-Henon-Lane-Emden-Conjecture-September-24-2026 The Subcritical Hénon–Lane–Emden Conjecture] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/370.md 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 <code>HenonEmden.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! 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'' ([https://arxiv.org/abs/2610.10188 arXiv:2610.10188]) || Extension (fractional) || For 0 < ''s'' < 1 and ''p'', ''q'' > 0, the system obtained by replacing −Δ with the fractional Laplacian of order 2''s'' has no strictly positive entire solution when 1/(''p'' + 1) + 1/(''q'' + 1) > (''n'' − 2''s'')/''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 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>HenonEmden</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-08 || [https://github.com/atimics/math2/blob/2c0f00528a8bb375d02bd48a513062254a53c285/docs/COROLLARIES.md atimics/math2], ''Cross-family corollaries of openai/math'', entry GE-8 (GitHub, commit <code>2c0f005</code>) || 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''|''A''''u''''p'' 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 [https://github.com/carlostoledo1891/cert-machine/blob/d93dd5b48e798372da73a42ac2275a3eeacd9a5e/corpus/openai-math/kernel-runs/38019899278/HenonEmden.json 38019899278] || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>HenonEmden</code> solution, in 803 s. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>HenonEmden</code>, so it was accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-13 || [https://github.com/mingfeng87/Lane-Emden-type-conjecture/tree/3069a7373cfe3ffcdbe14773179f49b5684f8170 mingfeng87/Lane-Emden-type-conjecture] (GitHub, commit <code>3069a73</code>) || 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 2''m'' with ''p'', ''q'' ≥ 1, ''pq'' > 1 under (''N'' + ''A'')/(''p'' + 1) + (''N'' + ''B'')/(''q'' + 1) > ''N'' − 2''m''. || 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'' ([https://arxiv.org/abs/2610.22802 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, [https://arxiv.org/abs/2610.27875 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.

[[Category:OpenAI results]]

The Lane–Emden conjecture - Revision history

Aftermath bot: New page: the Lane–Emden conjecture, from public sources; Main link