MathematicsTheoretical result
A Spectral Proof of Khachiyan's Ellipsoid Conjecture
About this illustration
A central slice through an inscribed ellipsoid
The blue ellipsoid represents the largest one that fits inside a convex body. The transparent plane represents a halfspace boundary through its center. This image introduces the paper's central-cut geometry; it is not an exact volume calculation, sharp cone family, or proof certificate.
Source · Abstract · maximum-volume ellipsoid and central halfspace cutThe idea, in plain language
A central cut meets a sharp ellipsoid limit
- What it is
- A paper claims the sharp largest-ellipsoid-volume bound after any halfspace cut through the ellipsoid’s center.
- Who did it
- Zhou Longfei, Haijun Zou, and Tianhao Liu.
- What it could mean
- A clean geometric slicing rule may become both mathematically settled and formally checkable, clarifying how much of a maximally inscribed ellipsoid can survive a central cut.
The claim
What the paper says.
The inspected abstract states a dimension-uniform sharp bound for central halfspace cuts of the maximum-volume inscribed ellipsoid, says an AI language model discovered the proof in a human-directed process, and reports Lean 4/mathlib verification of the main theorem, sharpness, and supporting results. It is a concrete theorem plus a claimed machine-checkable route, not a general-purpose optimization claim.
Why we tracked this work
a fresh source-backed convex-geometry theorem with an explicitly named Lean 4/mathlib formalization. Intake does not independently establish its matrix reductions, spectral bounds, sharpness family, or formal-artifact correspondence.
Why it matters
Foundational Convex geometry · Formal verification · AI-assisted proof
What could change?
Every convex shape has a largest ellipsoid that fits inside it. This paper claims a universal limit on how much of that ellipsoid remains after slicing through its center—and says the bound cannot improve.
If it holds up
It would settle Khachiyan’s conjecture with a sharp, dimension-independent geometric inequality and a reported Lean verification route.
If it does not
The failed reduction or sharpness argument would identify which geometric condition needs repair.
The evidence
What is on the record?
Discovery recorded. State of Proof has not yet examined this claim.
- Source
- A Spectral Proof of Khachiyan's Ellipsoid Conjecture Mathematical research record · Source record; see version
- Version
- submitted 2026-09-23 17:44:59 UTC
- Evidence reported
- Manuscript; independent examination not started
- Available artifacts
- arXiv links a Lean 4/mathlib formalization. No repository, TeX source, Lean project, theorem declaration, or proof script was downloaded, executed, or replayed.
- Highest-risk dependency
- The sharp constant depends on the precise normalization and central-cut hypothesis. A Lean claim or a spectral inequality excerpt cannot by itself establish that the formal statement matches every geometric condition and sharpness assertion in the manuscript.
What comes next
The next independent check.
Source-lock the exact halfspace, ellipsoid-center, and volume conventions; trace the abstract's positive-definite-matrix reduction, directional rank-one estimate, and sharp circular-cone family; then separately inspect the linked Lean theorem statement and its imports in an isolated environment.
How validation works