Equiregular counterexample to the sub-Riemannian Sard conjecture
Claude Opus 5/5.5 wrote the construction and first proofs, Lean-formalized with Codex (Wang, Zelenko)
Awaiting review
The takeaway
Lerario, Rizzi and Tiberio had disproved the sub-Riemannian Sard conjecture with a degenerate distribution, which left the natural equiregular case open. Wang and Zelenko close it with a rank-two distribution in dimension nine. Zelenko proposed the strategy; Claude generated the explicit structure and first proofs; the main theorems are fully formalized in Lean.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- 3 of 5
- Last verified
- 20 October 2026
Your AI and this story
- GPT-6 Astra169 days after its cutoff
- Claude Opus 5.5108 days after its cutoff
- Gemini 4 Argon199 days after its cutoff
- Grok 4.7138 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 108 days before it.
Key facts
- Paper: ‘An equiregular counterexample to the Sard conjecture for sub-Riemannian endpoint maps’, Bangjie Wang and Igor Zelenko, arXiv 2610.24080 [math.DG], 16 Oct 2026
- Result: equiregular rank-two distribution on an open set ≅ R⁹ with small growth vector (2, 3, 5, 8, 9), ‘maximal and generic for rank-two distributions in dimension nine’, whose endpoint map has no regular values. The earlier Lerario–Rizzi–Tiberio counterexample (rank two on R⁴) ‘is neither equiregular nor real-analytic’
- Announced, proofs deferred: an equiregular counterexample in dimension twelve with constant Tanaka symbol, to appear in a separate paper
- AI disclosure (follows the Leiden Declaration), verbatim: ‘The mathematical implementation of this strategy was generated in September and October 2026 in interactive sessions with Anthropic’s Claude [Claude Opus 5 and Claude Opus 5.5], used through the Claude desktop application. This includes the explicit structure (1.2), the first versions of the proofs of Theorems 1.1–1.3, in particular the formulation and solution of the moment problem of Sections 4–6, the statements in Appendices A and B, the explicit dimension-twelve structure announced in Appendix A, and first drafts of most of the text’. ChatGPT (6 Astra) later reviewed drafts against the formalization reports
- Human role: the lifting strategy and the Tanaka-symbol and abnormal-dynamics questions came from Zelenko; ‘Both authors checked all arguments line by line’; Sections 4–6 replace a single section of the AI draft
- Lean: Wang formalized Theorems 1.1–1.3 in Lean 4.30.0 / Mathlib with Codex; ‘The development contains no unproved statements and uses only the standard axioms’; Appendices A and B are not formalized; the formalization ‘detected two defects in an earlier draft’. Sources: Zenodo 10.5281/zenodo.23310061. The formal statements were written by the authors, who checked that they match the paper
What happened
The Sard conjecture in sub-Riemannian geometry asks whether the endpoints of abnormal (singular) horizontal curves form a set of measure zero. Lerario, Rizzi and Tiberio found a counterexample, but it relied on a degenerate distribution. Zelenko suggested lifting their example to higher dimension so that it becomes equiregular. Claude worked out the explicit structure and the hard analytic moment problem. The authors rewrote the analytic core, and Wang formalized the main theorems in Lean with Codex.
Why it matters
It shows that the failure of the Sard property is not caused by degenerate growth. It is also one of the most detailed AI disclosures so far, listing which parts came from Claude, which from the humans, and what the formalization caught.
What is disputed or not yet verified
| Verification | Unrefereed preprint; complete Lean 4 formalization of Theorems 1.1–1.3 (author-written statements) on Zenodo |
|---|
Sources
2 sources from 2 sites. Numbers match the chips in the text.
2 sources: 2 primary
Primary
Changes
- Filed (PDF read in full text)