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.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A Spectral Proof of Khachiyan's Ellipsoid Conjecture ↗See the proposed checks
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.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
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.
Read the source · Abstract · maximum-volume ellipsoid and central halfspace cut ↗- What it claims
- 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 this could matter
- A central cut meets a sharp ellipsoid limit 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.
- Impact horizon
- Foundational · Convex geometry · Formal verification · AI-assisted proof
- Version
- submitted 2026-09-23 17:44:59 UTC
- Why we tracked it
- 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.
- 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.
- 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.
- Current boundary
- Intake record only; examination not started.