--- id: "2026-10-16-sub-riemannian-sard-equiregular-counterexample-claude" url: "https://postcutoff.com/e/2026-10-16-sub-riemannian-sard-equiregular-counterexample-claude/" as_of: "2026-10-20T07:28:00+02:00" date: "2026-10-16" date_precision: day category: science importance: 3 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 2 editor: human editor human_review: null version: null --- As of: 2026-10-20 07:28 CEST. Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/ Canonical page: https://postcutoff.com/e/2026-10-16-sub-riemannian-sard-equiregular-counterexample-claude/ # Equiregular counterexample to the sub-Riemannian Sard conjecture Full title: 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) arXiv 2610.24080 (16 Oct 2026) by Bangjie Wang and Igor Zelenko constructs an equiregular rank-two distribution on an open set diffeomorphic to R⁹, with growth vector (2, 3, 5, 8, 9), whose endpoint map from the origin has no regular values. This settles the equiregular case left open by Lerario, Rizzi and Tiberio's disproof of the Sard conjecture of Zhitomirskii and Montgomery. Zelenko proposed lifting their example; "the mathematical implementation of this strategy was generated … in interactive sessions with Anthropic's Claude [Claude Opus 5 and Claude Opus 5.5]". Theorems 1.1–1.3 are formalized in Lean 4 with Codex, with no unproved statements. Unrefereed. ## 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 ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 169 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 108 days after its cutoff - Gemini 4 Argon (training cutoff March 2026): 199 days after its cutoff - Grok 4.7 (training cutoff May 2026): 138 days after its cutoff ## Sources 1. [arXiv 2610.24080: An equiregular counterexample to the Sard conjecture for sub-Riemannian endpoint maps](https://arxiv.org/abs/2610.24080) (arxiv.org, paper) 2. [Zenodo: Lean 4 formalization (10.5281/zenodo.23310061)](https://doi.org/10.5281/zenodo.23310061) (doi.org, code) ## Changes - 2026-10-20 (filed): Created (PDF read in full text) ## Related - 2026-10-20: [AI-assisted results in the 20 Oct 2026 arXiv listing](https://postcutoff.com/e/2026-10-20-ai-assisted-results-october-20-listing/index.md) - 2026-06-02: [Leiden Declaration on Artificial Intelligence and Mathematics sets community norms for AI in maths (4,000+ signatories)](https://postcutoff.com/e/2026-06-02-leiden-declaration-ai-mathematics/index.md)