--- id: "2026-10-26-ai-assisted-results-october-26-listing" url: "https://postcutoff.com/e/2026-10-26-ai-assisted-results-october-26-listing/" as_of: "2026-10-30T13:42:00+01:00" date: "2026-10-26" date_precision: day category: science importance: 2 confidence: medium status: [Awaiting review] verification: Lean-verified sources: 22 editor: human editor human_review: null version: "2026-10-27" --- As of: 2026-10-30 13:42 CET. 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-26-ai-assisted-results-october-26-listing/ # AI-assisted results in the 26 Oct 2026 sweep Full title: AI-assisted results in the 26 Oct 2026 sweep: Claude-written Lean proof of a frame-indifferent rank-one convex function that is not quasiconvex, a sculptor and Claude Code prove Takemura's conjecture, Claude's contribution to deterministic root-finding, and Zenodo records Catalogue of AI-disclosing papers from the 26 Oct 2026 arXiv announcement and recent Zenodo records not covered by their own entries. Highlights: Conti, Dolzmann and Dondl construct a frame-indifferent, rank-one convex but not quasiconvex function on ℝ³ˣ³, with a Lean 4 proof "produced entirely by" Claude Opus 5.5. A sculptor, Werner Alois Stanggassinger, proves Takemura's conjecture on Turk's head links with Claude Code. Spaenlehauer credits Claude Opus 5.5 with a link to an Erdős–Graham question in his deterministic root-finding paper. Søren Riis posts a new almost-entropic Ingleton-violation record with a Claude-written Lean proof. ## Key facts - Own entries: propeller conjecture (Heilman, 2610.32158), Tokareva's conjecture (2610.32239), triangle lower tail (2610.32879), graph-connectivity communication complexity (2610.32346). Enriched: Borodin–Kostochka (new Zenodo version, Δ ≥ 1000), mt0-svg (Calegari's U₃-slopes conjecture, Lean), BootLoops (Science news feature). OpenAI's 26 Oct release: ETH and local-smoothing/Kakeya entries - Frame-indifferent rank-one convex, not quasiconvex function in 3D (Sergio Conti, Georg Dolzmann, Patrick Dondl; Bonn, Regensburg, Freiburg; 2610.31886): explicit W : ℝ³ˣ³ → ℝ with W(QF) = W(F) for Q ∈ SO(3), quartic in the strain near SO(3), failing quasiconvexity at the identity by a third-order Šverák-type mechanism. AI statement (verbatim): Claude Opus 5.5, 'accessed through the agentic coding tool Claude Code', was used '(i) to write the Lean 4 formalization of Theorems 1.1 and 2.1, which was produced entirely by the model, with guidance from the authors on the statements and the proof strategy; and (ii) to assist in the development of the construction and of the proofs'. Lean repo github.com/sergioconti/so3-r1c-and-not-qc - Takemura's conjecture on Conway polynomials of Turk's head links Th(p,q) and Th(q,p), all p, q (Werner Alois Stanggassinger, 2610.32269; Zenodo since 6 Oct). The title-page note (verbatim): 'the choice of problem, the direction of the work and the computing hardware are due to the author (a sculptor); the formalisation, the algorithms and the proofs were developed by Claude Code (Anthropic) working with the author.' The problem came from a Claude Code literature search of the Di Prisa–Şavk survey, and Claude Code wrote the text and the SageMath checks. Takemura (2016) had proved q = 2, 3 - Deterministic root-finding over finite fields with elliptic curves (Pierre-Jean Spaenlehauer, Université de Lorraine/CNRS/Inria; 2610.32508): an unconditional deterministic online phase whose cost depends on the largest prime factor Ξ(D) of |E(F_q)|·|Ẽ(F_q)|; polynomial time would follow from a conjectured small-Ξ datum, which remains open. AI statement (verbatim): 'a complete earlier version of this paper … was written without any such tool … a few scientific contributions are to be credited to Claude Opus 5.5: the connection between Conjecture 1.5 and the question of Erdős and Graham on sums of two smooth integers, and the heuristic estimate based on the Dickman function that supports this conjecture' - Viterbo conjecture with quaternion symmetry (Julian Chaidez, Shira Tanny; 2610.31906): the weak Viterbo conjecture for Q-symmetric convex bodies in ℝ⁴, answering a question of Haim-Kislev–Ostrover. 'ChatGPT assisted in formalizing the construction in Section 4. ChatGPT also proposed Lemma 5.16.' - Pylyavskyy's positivity conjecture for arborescence ratios of covering digraphs (Muchen Ju, Junjie Ni, Kaixin Wang, Yihan Xiao; 2610.31980): partial ideas date from PACE 2024; 'Recently, GPT-6 Astra proposed extending the induction to finite-fiber systems, which allowed the proof to be completed.' - Corrected BMV pinching conjecture for all symmetrized word averages (Trung Hoa Dinh, Cong Trinh Le, Trung Dung Vuong; 2610.31851): ChatGPT used to 'examine known counterexamples' to the refined BMV conjecture, which led the first author to the corrected conjecture; in this paper it was used for literature, calculations and 'exploration and checking of possible arguments' - Foulon conjecture / higher-order periodic-orbit asymptotics for volume-preserving Anosov flows (Andrey Gogolev, 2610.31823): 'AI help (first Claude Opus 4.8 and then ChatGPT Sol 5.6) became invaluable for doing calculations'; ChatGPT pointed to a Gonchenko lemma that finished the hardest step; Claude and ChatGPT wrote 'initial drafts on most of the proofs', which the author substantially rewrote - Classical leash for an entire quantum computer (Yael Tauman Kalai, Dakshita Khurana, Justin Raizes; 2610.31775): resolves classical verification of quantum sampling with negligible soundness error and remote state preparation. 'We thank ChatGPT 6 for pointing out this attack and suggesting the fix via input encoding'; also: 'ChatGPT 6 has claimed a construction of this primitive, thereby lifting the result to negligible simulation loss. We are in the process of evaluating the claim.' - Exact covering numbers via links of minimum degree (Alfonso Gippini Requeijo, Team Banzai; 2610.31696): Claude (Opus 5.5, Fable 5.1) and GPT-6 Astra wrote the encoders, enumerators, checker and drafts, and 'took part in finding the arguments, among them the classification of Lemma 11' - Follow-ups to OpenAI release claims: Long–Zou, 'On the Allen–Cahn equation' (2610.28080 v2, 23 Oct), prove finite Morse index ⇒ O(R^(n−1)) energy growth for 4 ≤ n ≤ 9 'using the framework developed by OpenAI', citing OpenAI's manuscript 'A positive resolution of De Giorgi's conjecture in dimension eight' (family 375, 26 Sept; not previously covered here); 'The authors acknowledge the use of AI tools'. Hasratyan–Ruszinkó on the Erdős distinct subset sums problem (2610.32580) cite the problem as 'claimed to be disproved by GPT-6 Astra in 2026' and give new proofs of known bounds (no AI statement) - Smaller or supporting roles: Hardy–Littlewood asymptotic for primes p, p+4 from a uniform zeta-ratios conjecture (SeungJu Lee, 2610.32672: 'GPT was used in generating proofs.'); Calabi–Yau and Sullivan conjectures for minimal surfaces with symmetries (Alarcón, Forstnerič, 2610.31847: GPT 6.1 Sol to 'verify mathematical correctness and completeness'); cubic NLS with nonlinearity on a hypersurface (Chen, Huang, 2610.32180: 'acknowledge the use of AI tools'); acyclic 2-edge-coloured graphs (Bang-Jensen, Bessy, Reinald, 2610.32954: ChatGPT 6 Astra and Claude Opus 5.5 'for minor patches and proofreading') - Tools and agents: QuantumMatterExplorer (Nys, Jreissaty, Carrasquilla, ETH Zürich; 2610.32001), an LLM agent that maps quantum phase diagrams from its own DMRG runs cross-checked by exact diagonalization; PaperFormalizer (Tan, Syrgkanis, Blanchet, Stanford; 2610.31810), an author-in-the-loop pipeline in Claude Code or Codex that turns a paper into a Lean-verified version - Zenodo (AI-assisted, unrefereed): almost-entropic Ingleton score below −0.09738 (Søren Riis, record 23662511; previous constructions about 0.0925): 'Astra/Codex and Claude contributed mathematical development, computation and verification; Claude contributed the Lean formalisation and adversarial review. AI checks do not constitute independent human peer review.' Certified optimality of AlphaDev's sort3 (17 instructions) and sort4 (28) kernels (Zhiyang Chen, 23676958), with LRAT, Lean and Rocq certificates and Codex as an independent reviewer of pruning rules; sort5 left open. Markov uniqueness checked for z ≤ 10^500000 (Hu Tan, Ying Zhang, 23670834): 'OpenAI’s Codex was used extensively throughout this project', and the audit is 'an additional implementation check, rather than independent external replication' - Zenodo, not listed as results: about a dozen Lean 4 formalizations of classical plane-geometry and combinatorics theorems posted 26 Oct by Joshua Bald (Baranyai, Pascal, Cayley–Bacharach, Malfatti, Poncelet, Marden …), known theorems with no AI statement in the abstracts; Gregory Westberg's Lean rebuttals of the fringe 'VMS framework'. Skipped as unsupported claims: 'inconsistency of ZFC and PA' via strong Goldbach, a 'Master Ansatz' Hodge conjecture record, an E₈×E₈ octonionic neutrino model - Checked, no AI disclosure in the PDF: Hodge conjecture for generalized Kummer hyper-Kähler varieties of dimension 2n with n+1 prime (Floccari, Fu, 2610.31740), short proof of Zhang's stack-sorting conjecture (2610.32824), Faith's conjecture (2610.32544), real Jacobian conjecture criteria in ℝⁿ (2610.32391), Erdős–Straus for primes 24m+1 (2610.32302), semilinear Schrödinger with harmonic potential (2610.32274) ## What happened The 26 Oct arXiv announcement (papers submitted 22–23 Oct) and the day's Zenodo records were read in full where they disclose AI use (pdftotext). The quotes above come from the PDFs or the Zenodo records. The day's biggest maths news came from OpenAI's repository instead (ETH, local smoothing and Kakeya); those have their own entries. ## Why it matters Two things stand out in the tier below the headline results. First, Lean proofs written entirely by a model are becoming routine in applied analysis (Conti–Dolzmann–Dondl) and information theory (Riis). Second, a sculptor with Claude Code settled a published knot-theory conjecture. Papers following up on OpenAI's release (Allen–Cahn, distinct subset sums, propeller) are also starting to treat its results as given. ## What is disputed or not yet verified - Verification: Unrefereed arXiv and Zenodo preprints; Lean formalizations for 2610.31886 and the Riis and AlphaDev records ## Your AI and this story - GPT-6 Astra (training cutoff April 2026): 179 days after its cutoff - Claude Opus 5.5 (training cutoff June 2026): 118 days after its cutoff - Gemini 4 Argon (training cutoff March 2026): 209 days after its cutoff - Grok 4.7 (training cutoff May 2026): 148 days after its cutoff ## Sources 1. [arXiv 2610.31886: A frame-indifferent rank-one convex function in three dimensions which is not quasiconvex](https://arxiv.org/abs/2610.31886) (arxiv.org, paper) 2. [GitHub: sergioconti/so3-r1c-and-not-qc (Lean, written by Claude Opus 5.5)](https://github.com/sergioconti/so3-r1c-and-not-qc) (github.com, code) 3. [arXiv 2610.32269: Conway polynomials of Th(p,q) and Th(q,p): a proof of Takemura's conjecture](https://arxiv.org/abs/2610.32269) (arxiv.org, paper) 4. [arXiv 2610.32508: Deterministic root-finding over finite fields with elliptic curves](https://arxiv.org/abs/2610.32508) (arxiv.org, paper) 5. [arXiv 2610.31906: The Pu inequality and the Viterbo conjecture with finite symmetry](https://arxiv.org/abs/2610.31906) (arxiv.org, paper) 6. [arXiv 2610.31980: Coefficient positivity for arborescence ratios of covering digraphs](https://arxiv.org/abs/2610.31980) (arxiv.org, paper) 7. [arXiv 2610.31851: Positive planar measures for spectral pinching and the corrected BMV conjecture](https://arxiv.org/abs/2610.31851) (arxiv.org, paper) 8. [arXiv 2610.31823: Higher-order asymptotic formulae for Anosov flows and the Foulon conjecture](https://arxiv.org/abs/2610.31823) (arxiv.org, paper) 9. [arXiv 2610.31775: The Entire Quantum Computer on a Classical Leash](https://arxiv.org/abs/2610.31775) (arxiv.org, paper) 10. [arXiv 2610.31696: Links of minimum degree and exact covering numbers](https://arxiv.org/abs/2610.31696) (arxiv.org, paper) 11. [arXiv 2610.28080: On the Allen–Cahn equation (Long, Zou)](https://arxiv.org/abs/2610.28080) (arxiv.org, paper) 12. [arXiv 2610.32580: New approaches to the Erdős distinct subset sums problem](https://arxiv.org/abs/2610.32580) (arxiv.org, paper) 13. [arXiv 2610.32672: Hardy–Littlewood asymptotic for primes p and p+4 from a zeta-ratios conjecture](https://arxiv.org/abs/2610.32672) (arxiv.org, paper) 14. [arXiv 2610.31847: The Calabi–Yau and Sullivan conjectures for minimal surfaces with symmetries](https://arxiv.org/abs/2610.31847) (arxiv.org, paper) 15. [arXiv 2610.32180: Cubic NLS with nonlinearity supported on a hypersurface](https://arxiv.org/abs/2610.32180) (arxiv.org, paper) 16. [arXiv 2610.32954: Acyclic 2-edge-coloured graphs](https://arxiv.org/abs/2610.32954) (arxiv.org, paper) 17. [arXiv 2610.32001: QuantumMatterExplorer](https://arxiv.org/abs/2610.32001) (arxiv.org, paper) 18. [arXiv 2610.31810: PaperFormalizer](https://arxiv.org/abs/2610.31810) (arxiv.org, paper) 19. [Zenodo 23662511: An almost-entropic Ingleton score below −0.09738 (Riis)](https://zenodo.org/records/23662511) (zenodo.org, paper) 20. [Zenodo 23676958: Certified optimality of AlphaDev's sort3 and sort4 kernels](https://zenodo.org/records/23676958) (zenodo.org, paper) 21. [Zenodo 23670834: Computational verification of the Markov uniqueness conjecture for z ≤ 10^500000](https://zenodo.org/records/23670834) (zenodo.org, paper) 22. [arXiv 2610.31740: Hodge conjecture for hyper-Kähler varieties of generalized Kummer type (no AI)](https://arxiv.org/abs/2610.31740) (arxiv.org, paper) ## Changes - 2026-10-26 (filed): Created ## Related - 2026-10-26: [OpenAI claims ETH is false](https://postcutoff.com/e/2026-10-26-openai-eth-false-subexponential-sat-claim/index.md) - 2026-10-26: [OpenAI claims local smoothing and Kakeya in all dimensions](https://postcutoff.com/e/2026-10-26-openai-local-smoothing-kakeya-all-dimensions-claim/index.md) - 2026-10-25: [AI-assisted results in the 25 Oct 2026 sweep](https://postcutoff.com/e/2026-10-25-ai-assisted-results-october-25-listing/index.md) - 2026-10-23: [Heilman simplifies OpenAI's propeller conjecture proof](https://postcutoff.com/e/2026-10-23-propeller-conjecture-openai-proof-heilman-simplification/index.md) - 2026-10-23: [Tokareva's bent-function conjecture disproved by LLM agents](https://postcutoff.com/e/2026-10-23-tokareva-bent-functions-conjecture-disproved-minimax-agents/index.md) - 2026-10-23: [Triangle lower tail: Zhao's conjecture settled with GPT-6 Astra and Claude](https://postcutoff.com/e/2026-10-23-triangle-lower-tail-zhao-conjecture-gpt-6-astra-claude/index.md) - 2026-10-23: [Graph connectivity communication bound settled, with ChatGPT](https://postcutoff.com/e/2026-10-23-graph-connectivity-nondeterministic-communication-complexity-chatgpt/index.md) - 2026-10-20: [Borodin–Kostochka conjecture claimed for maximum degree ≥ 4583 (down from 5.3 million), then ≥ 1000 (26 Oct), with GPT-6 Astra assisting](https://postcutoff.com/e/2026-10-20-borodin-kostochka-threshold-4583-gpt-6-astra/index.md) - People: [Jensen Huang](https://postcutoff.com/person/jensen-huang/)