翻訳待ち：A graded registry of scientific results produced by or with AI

AI サービスが一時的に利用できないため、復旧後に翻訳を補完します。

INIndependent 2026-07-22 Claimed AI-led ModelGPT-5.6 Pro Fieldcomputer-science Posed1999 · open 27 yrs Counterexample to the Dinitz–Garg–Goemans conjecture# An explicit seven-node network whose cheapest single-route (unsplittable) shipping costs more than its fractional cost even under the allowed capacity slack, disproving a conjecture from the late 1990s. Dinitz, Garg, and Goemans proved that any fractional multicommodity flow can be rounded to an unsplittable (single-path-per-demand) flow while violating each arc's capacity by at most the maximum demand. Goemans conjectured this rounding could also be done without increasing the total cost. The counterexample is a directed graph on seven nodes carrying three demands (15, 10, 15); its fractional solution costs 58, yet every unsplittable routing that stays within the allowed capacity cushion (violation ≤ 15) costs at least 60. Rybin reached it with GPT-5.6 Pro in four short prompts and reported that the model returned proof certificates, an exhaustive-enumeration verification program, machine-readable data, and LaTeX source. WithDmitry Rybin combinatorial-optimizationnetwork-flowcounterexampleunsplittable-flow AnnouncedX↗ MediaOfficeChai↗ Challengenone linked Novelty check, caveats & sources Novelty check The Dinitz–Garg–Goemans unsplittable-flow result is from the late 1990s (D. Dinitz, N. Garg, M. Goemans, 'On the single-source unsplittable flow problem'); the cost-preserving strengthening was an open conjecture attributed to Goemans. No prior counterexample or resolution appears in the literature. The construction is a new concrete instance, not a retrieval of an existing example. Caveats Not peer-reviewed or machine-checked in a proof assistant. Verification rests on the author's own exhaustive-enumeration program over a finite instance, which anyone can rerun but which had no logged independent replication at announcement. The result was shared informally on X with a public GPT-5.6 Pro transcript. One third party (Hensen Juang) publicly generalized the instance into an infinite parametric family on the same seven nodes, which is consistent with the claim but is not a formal independent check. Autonomy graded ai-led: the model produced the construction; the human posed the problem and verified. Downgraded from 'author verified' when source classification showed no primary artifact is linked: the construction was published as a chat transcript rather than a paper or repository. Readers have checked the arithmetic and found it consistent, but there is nothing citable to point at, so the grade caps at 'claimed' until someone links a standalone write-up. Announcement XDmitry Rybin announcement (X)↗ Media coverage OfficeChaiCoverage: officechai↗ Community discussion XHensen Juang: infinite family generalizing the counterexample (X)↗ INIndependent 2026-07-20 Author verified AI-led ModelGPT-5.6 Sol Pro + Claude Fable 5 Fieldmathematics Posed2017 · open 9 yrs Counterexamples to the Gaussian moments conjecture# Explicit low-degree polynomials disproving a 2017 conjecture that had been proposed as a route to proving the Jacobian conjecture, found days after that conjecture was itself disproved. Derksen, van den Essen and Zhao proposed the Gaussian moments conjecture and showed that the Jacobian conjecture would follow from it. Long reports that a cubic counterexample in four variables was produced by GPT-5.6 Sol Pro with no human intervention after the initial prompt, which simply noted that the Jacobian conjecture had just been disproved and asked whether a small counterexample to GMC might therefore exist; Claude Fable 5 then found a quartic counterexample in three variables and supplied independent algebraic checks. Together these show GMC(n) is false for every n ≥ 3. WithChristopher D. Long algebrapolynomial-mapscounterexamplejacobian-conjecture Original workarXiv↗arXiv↗ Challengenone linked Novelty check, caveats & sources Novelty check The Gaussian moments conjecture is due to Derksen, van den Essen and Zhao (Israel J. Math., 2017), building on their earlier moment-vanishing and integral conjectures. No prior counterexample appears in the literature; the conjecture's interest was precisely that it implied the Jacobian conjecture, which was disproved on 2026-07-19. The two-variable case GMC(2) is explicitly left open by this paper. Caveats arXiv preprint, not peer-reviewed, single author. The constructions are explicit polynomials and checkable by computer algebra, which lowers the cost of verification, but no independent check is on the public record yet. The result is a corollary of the Jacobian collapse rather than an independent line of attack: the prompt that produced it began by telling the model that the Jacobian conjecture had fallen. Original work arXivSmall Counterexamples to the Gaussian Moments Conjecture↗arXivDerksen, van den Essen, Zhao: The Gaussian Moments Conjecture and the Jacobian Conjecture↗ Anthropic 2026-07-19 Formally verified Collaborative ModelClaude Fable 5 Fieldmathematics Posed1939 · open 87 yrs Counterexample to the Jacobian conjecture in dimension three# An explicit polynomial map in three variables with constant Jacobian determinant −2 that is nevertheless not invertible, disproving a conjecture open since 1939. The map F(x,y,z) = (u³z + y²u(4+3xy), y + 3xu²z + 3xy²(4+3xy), 2x − 3x²y − x³z) with u = 1+xy has Jacobian determinant identically −2, yet sends the three distinct points (0,0,−¼), (1,−3/2,13/2) and (−1,3/2,13/2) all to (−¼,0,0). A map with a global inverse cannot be three-to-one. Alpöge, a number theorist at Anthropic, announced it on X the day it was found. WithLevent Alpöge algebraic-geometrycounterexamplepolynomial-maps Original workjacobianfun.org↗ CommentaryAlexis Gallagher↗Hacker News↗ Challengenone linked Novelty check, caveats & sources Novelty check The Jacobian conjecture (Keller, 1939) has been a celebrated open problem for 87 years, with many published false proofs in both directions. No prior counterexample in any dimension over characteristic 0 exists in the literature. Ott-Heinrich Keller's original formulation is the one addressed. Caveats Not yet peer-reviewed. The formula is public and checkable in seconds by computer algebra, which makes conventional peer review less load-bearing than usual, but the official record lists the conjecture as open until the literature catches up. The division of labor between Alpöge and the model has not been fully documented; autonomy graded conservatively pending a transcript. Independent checks whataifound.org (symbolic recomputation, SymPy): confirmed, det J = −2 identically; all three points map to (−¼,0,0) Multiple mathematicians via public computer-algebra checks: confirmed · link ↗ Original work jacobianfun.orgThe Jacobian counterexample, explained↗ INIndependent 2026-07-14 Formally verified AI-led ModelGPT-5.6 Sol Pro Fieldmathematics Posed1996 · open 30 yrs Near-quadratic lower bound for derivative-free convex optimization# A lower bound of order d²/log d on the number of exact function evaluations needed to minimize a convex Lipschitz function, closing a gap open since 1996 and showing a 1996 algorithm was essentially optimal. In zeroth-order optimization an algorithm may only query a function's value, never its gradient. Protasov's 1996 algorithm needed about d² evaluations in d dimensions, but the best known lower bound was only about d, leaving open whether a much faster method existed. The new bound of Ω(d²/log(d+1)) matches the upper bound to polylogarithmic factors. Kerger reports that after a ten-page prompt built on his own earlier failed attempts, the model produced the complete proof in a single 2.5-hour session with no intervention; he then reviewed it and formally verified the core bound in Lean 4, which compiles against Mathlib with no sorry and no bespoke axioms. WithPhillip Kerger optimizationcomplexity-theorylower-boundslean Original workarXiv↗GitHub↗ Challengenone linked Novelty check, caveats & sources Novelty check The gap between Protasov's O(d²) upper bound (1996) and the O(d) lower bound is documented in the derivative-free optimization literature and had stood for three decades. No prior matching lower bound appears in the literature. The paper is explicit that the AI produced the argument. Caveats arXiv preprint, not peer-reviewed. The author states plainly that 'it is accurate to say that the AI model used solved the problem, not the author of this paper', which is the basis for the ai-led grade; the human wrote the prompt, reviewed the proof, and did the Lean formalization. Graded formal on the strength of the machine-checked Lean artifact for the core bound, not on the preprint as a whole. Independent checks Lean 4 / Mathlib compiler (author-run, artifact public): core Ω̃(d²) lower bound compiles with no sorry and no bespoke axioms · link ↗ Original work arXivClosing the Oracle-Complexity Gap in Derivative-Free Convex Optimization↗GitHubLean verification, prompt and chat logs↗ INIndependent 2026-07-11 Formally verified Collaborative ModelOpenAI Sol (construction); Claude Fable (Lean formalisation) Fieldmathematics Counterexample to Grothendieck's question on finite flat group schemes# A finite locally free group scheme of order four whose fourth power map is not trivial, answering a question Grothendieck raised in the 1960s; one model produced the construction and another formalised it in Lean. Grothendieck asked whether every finite locally free group scheme of order n is killed by n. Deligne proved it for commutative group schemes; the non-commutative case stayed open. The counterexample is a Hopf algebra of rank four over the ring Z[a,b]/(a³, b³, a²b+2), with coordinate algebra R[U,V]/(U² − abU + b²V, V² − a²V), whose fourth convolution power is not the convolution unit. Kevin Buzzard, told of a 12-page informal write-up, replied that he does not read AI-generated informal mathematics and asked for a Lean proof instead; four hours later a 1,076-line Lean formalisation existed, and it compiles on a laptop in under five minutes. It was submitted to mathlib as pull request #41748. WithAkhil Mathew, Kevin Buzzard algebraic-geometrygroup-schemescounterexampleleanformalization Original workGitHub↗ AnnouncedKevin Buzzard↗ Challengenone linked Novelty check, caveats & sources Novelty check Per Buzzard's account, the question had been settled in special cases by Grothendieck, Deligne and René Schoof, with further partial results published by Emiliano Torti in 2025; no counterexample appeared in the literature. The object here is an explicit new construction rather than a rediscovered example, and the Lean file states and refutes the general claim directly. Caveats The mathlib pull request was open, not merged, when this entry was written, and was filed by a pseudonymous account whose module docstring credits "Codex (OpenAI) and Claude (Anthropic), under the direction of the author" rather than naming Sol or Fable; the model attribution here follows Buzzard's blog post. The formal grade rests on the Lean proof compiling, which Buzzard reports doing himself; the 12-page informal argument has not been peer reviewed. Autonomy graded collaborative: a human posed the question, directed the work and filed the PR, and the record of who did which step is a blog post rather than a transcript. Independent checks Kevin Buzzard (compiled the Lean formalisation): confirmed; 1,076-line Lean proof compiles in under five minutes · link ↗ Original work GitHubmathlib4 PR #41748: a finite free group scheme of order four not killed by four↗ Announcement Kevin BuzzardHuman mathematicians are being outcounterexampled↗ VVesuvius Challenge 2026-06-25 Author verified AI-assisted ModelCommunity-developed ink-detection neural networks Fieldarchaeology First Herculaneum scr [truncated for AI cost control]