Double-cap conjecture claimed in all dimensions, with a separate AI-built Lean proof
Awaiting review
Importance: major (4 of 5)Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Major (4 of 5)
- Last verified
- 21 October 2026
Your AI and this story
- GPT-6 Astra173 days after its cutoff
- Claude Opus 5.5112 days after its cutoff
- Gemini 4 Argon203 days after its cutoff
- Grok 4.7142 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 112 days before it.
Key facts
- Claim (arXiv 2610.27523): ‘a measurable subset of S^(n−1) containing no orthogonal pair has measure at most that of two opposite open caps of radius π/4’, for n ≥ 3, with rigidity up to null sets; also the measurable fractional chromatic number of the spherical orthogonality graph
- History: Witsenhausen (Amer. Math. Monthly 1974) proved α_n ≤ 1/n; the double-cap conjecture α_n = δ_n is attributed to Kalai; the best earlier bound on S² was α_3 < 0.313
- AI statement (abstract): ‘AI played an assistive role in preparing this paper. The formalization and verification workflow for a separate Lean 4 proof of the main inequality and double-cap result, based on a different argument, were carried out almost entirely using AI-assisted tools.’
- Paper’s caveat: the Lean development ‘does not constitute a verification of the proof or the additional applications presented here’
- LeanShadow repo: 138 modules, sorry-free, standard axioms; Comparator matched 12 main results (incl. double_cap_conjecture, s2_double_cap_bound 1 − √2/2) against a reference challenge; Lean and nanoda kernels; formalization.yaml lists automation ‘agent, framework: Codex’ for packaging, adapters and tooling; review status ‘self-assessed’
What happened
The double-cap conjecture asks for the largest measurable set on a sphere that contains no two orthogonal points. Witsenhausen posed the problem in 1974, and Gil Kalai’s survey on Borsuk’s problem made it widely known. The conjectured answer is two opposite caps of angular radius π/4.
On 20 Oct 2026 five mathematicians from Fortaleza and São Paulo posted a proof for all n ≥ 3. It runs through a sharp “orthogonal neighbourhood” inequality in real projective space, proved with the Funk transform, rotation comparisons and second-variation arguments. A separate Lean 4 development (LeanShadow, public since 11 Sept 2026) proves the same main inequality and the double-cap result by a different argument. The authors say they built it “almost entirely using AI-assisted tools”, and its metadata names a Codex agent.
The paper is unrefereed, and the Lean proof was self-assessed. No expert reaction was found on 21 Oct.
Why it matters
If confirmed, a 52-year-old geometry problem falls in every dimension, and a machine-checked proof of the statement already exists. Experts can check that Lean statement against the classical formulation faster than a long analytic paper. This is another case of AI tools mainly turning a human result into a formally verified one.
What is disputed or not yet verified
| Verification | Unrefereed preprint; separate Lean 4 proof (different argument) with Comparator and two kernels, statements written by the authors, self-assessed |
|---|
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Filed (PDF, LeanShadow README and formalization.yaml read)