Gaussian product inequality conjecture proved
For any centered Gaussian vector and positive exponents, the expectation of the product of absolute powers is at least the product of the individual expectations, settling a conjecture posed in 2007.
- Lab
- Independent
- Model
- ChatGPT 5.6 Sol
- Field
- Mathematics
- Date
- 2026-07-20
- Human collaborators
- Frédéric Ouimet, Dylan Greaves
- Problem posed
- 2007 · open 19 yrs
Sources
Original work
Announcement
Independent commentary
What was found
The conjecture states that for a centered Gaussian vector X = (X_1..X_n), not necessarily nondegenerate, and any positive exponents a_1..a_n, the expectation of the product of |X_i|^a_i is at least the product of the expectations of |X_i|^a_i. The stronger form adds that when every variance is positive, equality holds exactly when the coordinates are independent. The model returned a complete and correct solution from Greaves's prompt. It did not include the equality characterization, but only because that case was not in the prompt as posed. The proof was formalized in Lean using Codex, and the full prompt and output are public as a shared chat transcript.
Novelty check
The Gaussian product inequality is a named conjecture dating to 2007, with a substantial partial-results literature covering special cases such as even integer exponents and small dimensions; it was recorded as open in the general case. The proof settles the general statement. No prior general proof appears in the literature.
Caveats and known objections
Not peer-reviewed; released as a preprint with a public chat transcript rather than through a journal. The Lean formalization is author-produced. The AI output omitted the equality-characterization half of the strong form, which was supplied around it. Checks by other models (ChatGPT 5.6 Sol Pro, Gemini 3.1 Pro, Grok 4.5) are not independent human verification and do not raise the grade; the human check by Ouimet is author-side.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Gaussian product inequality conjecture proved. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-20-gaussian-product-inequalityBibTeX
@misc{whataifound-independent-2026-inequality,
title = {Gaussian product inequality conjecture proved},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-07-20-gaussian-product-inequality}
}