What AI has
actually contributed

This is a formalization, not a new theorem, and the entry is graded as such. Wiles and Taylor-Wiles proved Fermat's Last Theorem in 1995; nothing mathematically new is claimed here, and Kevin Buzzard states directly that 'mathematically this work of anthropic tells us essentially nothing' and that 'the formalization just faithfully follows the early literature on the proof and adds nothing'. What is new is the scale of autoformalization: prior partial formalizations existed, notably the ongoing Imperial College FLT project this work builds on, and no complete machine-checked proof of the theorem existed before. It completes the last open item of Wiedijk's list of 100 theorems.

The result is a formalization of an existing proof and should not be read as new mathematics. Verification is graded formal on the machine checks rather than on the announcement: the comparator check ties the proved statement to Mathlib's own, and a second independent kernel replayed it. What no tool establishes, and the repository says so itself, is that each intermediate theorem means what its name suggests, since names are machine-generated and 'where a name and a statement disagree the statement is what was proved'. Buzzard reports the codebase is over 13.4 million lines and that the proof as formalized only works for exponents p at least 17, with smaller cases covered by earlier work. Reproducing the checks is expensive: the build takes hours at 96 jobs with a peak of 153 GB of memory, and the comparator run about 15 hours. Autonomy is graded ai-led rather than autonomous: the announcement describes Claude working 'largely autonomously' but also records high-level human steering from Tianyi Peng, and the strictest defensible reading applies.

The Koethe conjecture has stood since 1930 and is stated as open in Google DeepMind's Formal Conjectures at the commit the harness pinned, which is what the model was given. Krempa's 1972 equivalences are the standard literature on the problem and are cited in the repository. No prior disproof of the matrix form, and no prior resolution of the conjecture in any of its equivalent forms, was found in the four registries or the surrounding literature. What is new is the counterexample and its Lean proof, not the equivalence, which is classical.

The machine-checked statement is Krempa's matrix form, not Koethe's original question, and the step from one to the other is a 1972 equivalence in the literature rather than part of what was checked. Anyone citing this as a disproof of the Koethe conjecture is relying on that equivalence, and an algebraist should confirm it holds in the form used. The repository is prepared for submission to Palomar but no registration had landed at entry, and no expert in ring theory is on record as having read the construction. The verification grade rests on the mechanical check of the matrix-form statement, which vibemathed independently cloned and confirmed at 3,331 lines with no sorry outside the statement stub and no axiom declarations. Autonomy is graded autonomous on the repository's explicit record that the run was one attempt per statement with 'no human saw or steered the proof search', the only human input being the pre-existing benchmark statement; the repository also discloses that the whole repository was machine-written by AI assistants at Adamczewski's direction.

The conjecture dates to 1962 and is Erdos Problem 548. The weaker statement with (k-2)n edges is an easy induction, and the repository records that the conjecture was previously proved for large k by Ajtai, Komlos, Simonovits and Szemeredi, work that has not appeared in full. The formalized statement is the benchmark's, stated as open in Formal Conjectures at the pinned commit. No prior full formal proof was found in the four registries. The novelty question here is less about priority than about scope, and the scope limit is recorded in the caveats rather than left implicit.

The formalized statement is very slightly weaker than the classical conjecture, and the repository documents the gap precisely rather than glossing it: when (k-1)n is odd, more than (k-1)n/2 edges is already satisfied with one edge fewer than at least (k-1)n/2 + 1 requires, so in that parity case the compared theorem assumes half an edge more. The classical statement implies the formalized one and not conversely. The repository notes that the proof's internal counting lemma derives the sharp classical bound, but only the weaker advertised form is what the comparator compares, so the machine-checked claim is the weaker one and this entry is worded to it. No expert in extremal graph theory is on record as having read it, and the Palomar submission had not landed at entry. Autonomy is autonomous on the same disclosure as the Koethe entry: one attempt, no human seeing or steering the proof search.

The irrationality of Catalan's constant is a well-known open problem with no claimed resolution in the four registries before this preprint. The method is explicitly derivative of Calegari, Dimitrov and Tang's 2024 work, which the paper cites, and the claimed novelty is the weighting construction rather than the framework. No competing claim was found. The question of priority is not the issue here; the correctness of the argument is, and it is disputed.

Graded disputed on a specific, unresolved technical objection rather than on general scepticism. The objection, raised publicly and cited here, is that the tail recurrence of equation 1.4 is inconsistent with the factor used in equation 2.12, so the zero count the argument needs in order to force the degree bound fails. The same critique notes that the paper replaces the arithmetic content of the model it follows with a combinatorial minimization plus numerics that no human has checked, and points to internal inconsistencies in the write-up. The preprint remains at version one with no revision or withdrawal at entry. Autonomy is graded ai-assisted, and the paper's own account is the reason: the model 'made many attempts but we failed again and again' until 'the author realized that we should use suitable weights', so the decisive idea is the author's. The only stated verification of the whole proof is by a language model, which is not an independent check by any human.

Whether QMA(2) collapses to QMA has been tracked since Watrous posed the no-disentanglers conjecture, reported by Aaronson, Beigi, Drucker, Fefferman and Shor in 2009. The paper cites the prior partial results it improves on: Harrow, Natarajan and Wu obtained a quasipolynomial lower bound when the error is exponentially small, and Akibue, Kato and Tani proved an exponential lower bound for the more restrictive strong disentanglers. No prior oracle separation was found. The result is new, and is an oracle separation rather than an unrelativized one.

An unrefereed preprint days old at entry, with no formalization and no independent check. The separation is relative to a quantum oracle and does not settle whether QMA(2) equals QMA in the unrelativized world. Autonomy is graded ai-assisted rather than ai-led on the strictest defensible reading of the paper's own account: the authors state that 'the proof idea underlying the main theorem was generated using ChatGPT 5.6 Sol', but also that their initial prompts directed the model to the work of She and Yuen and that they 'subsequently verified, simplified, and developed the argument presented here, and take full responsibility for its correctness'. Humans chose the problem, supplied the key reference and did the development. No transcript has been released, so the phrase 'minimal additional guidance' cannot be checked.

The conjecture is named and dated to 1983, due to David E. Daykin and Peter Frankl, and no prior proof was found in the four registries or the surrounding literature on the Boolean lattice. The note presents itself as a first proof rather than a rediscovery, and the strengthened product inequality it proves does not appear in the prior literature located. The result is new.

A four-page unrefereed preprint, checked by its human author and by nobody independent, with no formalization. The human role as stated is verification and communication rather than discovery, which is why autonomy is graded ai-led: the model produced the proof content and the author checked and wrote it up. The model is named in the note's body rather than the abstract. What 'verify' amounts to here is not spelled out, and for a short combinatorial argument the distinction between a careful check and a read matters; treat the proof as needing an independent reading.

The conjecture is attributed to Andrzej Trautman and dated 1998, and the paper's introduction sets out its origins and the standard nonembeddability constructions it modifies. No prior counterexample was found in the four registries or in the CR geometry literature located; the point of the paper is that the existing nonembeddable examples do not preserve the closed canonical section, which is exactly what the modification supplies. The result is new.

A single-author unrefereed preprint days old at entry, labelled by its author a preliminary version, with no independent check and no formalization. The AI disclosure sits in the acknowledgements rather than the abstract, which is the pattern worth noting: a reader of the abstract alone would not know a model was involved. Autonomy is graded ai-assisted on the strictest defensible reading. The acknowledgements say 'The counterexample construction presented below was discovered through experimentation using ChatGPT Plus on August 18, 2026' and that ChatGPT also drafted the manuscript and helped proofread, but the framing is the author's experimentation, the problem was posed to him by Pawel Nurowski and Rod Gover, and he states he 'independently checked all calculations and arguments presented here and takes full responsibility'. A case for ai-led could be made from the word discovered; the weaker grade wins.

The question is named, dated and attributed to McKean in 1966 in the paper's own opening, and the parameter range is chosen precisely so that the two classical models, hard spheres and Maxwell molecules, are covered. The paper separately flags the corresponding question for the Landau equation as still open, which shows the boundary of the claim is being drawn deliberately. No prior counterexample appears.

A preprint days old at entry, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-led on the paper's disclaimer on the use of AI tools, which records a chain of tools and a substantial human rewrite: a first version of the proof was obtained by ChatGPT 5.6 Sol, run in Codex in Ultra mode with access to the source of one of the author's own earlier papers and other notes, and it was then rewritten first using Claude Code and afterwards reinterpreted and restructured by the author.

Both conjectures are named, attributed and dated in the paper: Burness and Giudici for base size two in 2020, and Freedman, Huang, Lee and Rekvényi for the extension to arbitrary base size. The counterexamples are exhibited as explicit infinite families rather than existence claims, and their spread across three of the five O'Nan-Scott types is stated precisely. The Kourovka Notebook problem answered here is 21.29, which is not among the eight problems covered by this registry's existing Kourovka entry. No prior counterexample appears.

A preprint days old at entry, unrefereed, with no independent human check on record. The formal grade rests on Theorem 1.2, the statement that counterexamples exist at every base size, which is verified in Lean 4 with no sorry placeholders and no project-specific axioms, with the source in the paper's repository; the three additional base-size-two families and the diameter computations are not covered by that formalization, and the Lean statements have not been audited by a third party against the paper. Autonomy is graded collaborative on a detailed disclosure describing back-and-forth rather than handoff: the project began with Codex support aimed at proving the conjecture for soluble affine groups, the authors then worked with Codex, ChatGPT Pro and Claude to find further examples and constructions, search the literature and draft the manuscript, Codex implemented much of the Magma, GAP, Python and C++ code, and the Lean formalisation was produced primarily by Codex with the authors reviewing its theorem statements and verifying the completed formalisation.

The conjecture is a named open question in classification theory, attributed in the paper to Hart, Kim and Pillay (1996) and described there as long-standing. The construction runs through the standard route for such results, proving simplicity and then characterising forking independence via the Kim-Pillay criteria, so its relation to the existing literature is explicit rather than assumed. Model-theoretic study of noncommutative rings has precedent, which the authors cite; no prior counterexample appears.

A preprint days old at entry, unrefereed, not formalized, and with no independent check on record. Autonomy is graded collaborative rather than ai-led on the authors' own account of the division of labour: they prompted the model with a detailed series of prompts that encoded the known restrictions such a counterexample must satisfy, and specifically directed it to the standard strategy of proving simplicity and applying the Kim-Pillay criteria, so the framing was substantially theirs. They state that the proofs of the relevant facts and aspects of the setup were written entirely by the authors and that no AI tool was used in writing the manuscript, with AI used for proofreading under manual evaluation. They also record their view that the counterexample would have been unlikely to be found in the near term without generative AI.

The open question is attributed to Boyar and Find and dated 2014, and the paper is explicit about what the classical bounds do and do not settle: they cover bilinear and quadratic models, not unrestricted Boolean circuits with nonlinear reuse. That distinction is the entire content of the contribution and is stated before the result. No prior unrestricted lower bound for this function appears.

A preprint days old at entry, unrefereed, with no independent human check on record, and vibemathed records the resolution as partial since this settles one function rather than the general question. The formal grade is well supported for a self-published result: the Lean 4 formalization covers the Boolean-ANF semantics, the unrestricted circuit model, the seven- and eight-gate exclusions and the explicit nine-gate upper bound, uses no project-specific axiom and no native decision procedure, pins Lean v4.32.1 and a locked mathlib revision, and its continuous integration performs the build, an axiom audit and a declaration replay with a weekly fresh source replay. What is missing is third-party auditing that the formalized statements say what the paper says. Autonomy is graded ai-assisted, matching the disclosed roles, with GPT-5.6 Sol at an extra-high setting and Claude Opus 5 acting as a referee.

The repository is explicit that the problem remains open and that what is proved are criteria and instances rather than the general statement, so the novelty question is about the criteria rather than the headline. Every compared statement that concludes Problem 10.61 does so in a quadratic setup, and both worked instances are quadratic, because the covering criterion is proved only there; the arbitrary-degree material does not carry any compared statement above degree two. That boundary is recorded in the registry entry as well as in the repository.

Announced through a repository rather than a paper, unrefereed, with no independent check on record. The grade is claimed rather than formal despite a Lean development, because what is machine-checked covers the quadratic criteria and instances rather than the problem, vibemathed records the Lean work as checked with its statement unaudited, and the covering criterion additionally leaves cases open even within the quadratic range. Anyone citing this should treat Problem 10.61 as open. Autonomy is graded ai-led following the registry's record of the models as the source of the results, with the repository owner supplying framing and publication; no author-written AI disclosure has been located.

The landscape is fixed by an independent recent paper rather than by the claimant: Luo, Ma and Zhao (arXiv:2601.13552) state in their own abstract that the conjecture was known for k in {3, 4} and prove it for every k at least 6, which identifies k = 5 as the remaining case at the time of writing. No competing resolution of k = 5 appears in that literature or in the vibemathed record. The claim is new work on an identified gap.

A Zenodo preprint days old at entry, unrefereed, with no independent check on record. The computer-assisted part is the narrow part: nine finite configuration families have verifiers and certificates, and certificate runs are reported as passing, but the reductions from arbitrary graphs to those finite state spaces are ordinary prose arguments that are not machine-checked and that only the submitter has audited. That is why the grade is claimed despite the artifact. Autonomy is graded ai-led rather than autonomous because a human submitted, framed and archived the work; the Zenodo record names Elias Botsford as the sole creator, a detail the registry rows carrying this result omit.

The baseline chain is named and dated in the paper: 2.753 from Charikar, Ramakrishnan, Wang and Wu in JACM 2024, then 2.5 independently by Frank (arXiv:2608.17863) and Ye (arXiv:2608.21202) weeks before this work. The paper also states why 2.5 was a barrier rather than merely the current best, namely that no mixture of the two rules involved yields a better bound, which is what the new lottery is introduced to get past. No stronger bound appears.

A preprint days old at entry, unrefereed, not formalized, with no independent check on record, and vibemathed records it as a partial result since the optimal distortion remains unknown. Autonomy is graded ai-led on a disclosure that describes the model producing the key ideas under human guidance: all proofs in the document were obtained using GPT-5.6 Sol with guidance from the author, who verified them for correctness and expanded and simplified the exposition with the aid of GPT-5.6 Sol and Claude Opus 5. The author records two specific steps where the model autonomously identified the ingredient to add, first a stable lottery and then a lottery whose existence it proved by a minimax argument.

The result was known for dimension two by Harris and Kesten and for dimension at least eleven by the lace expansion of Hara and Slade and of Fitzner and van der Hofstad; the repository cites Grimmett's Percolation and Duminil-Copin's 2018 ICM conjecture for the standing of the open cases 3 to 10. The proved statement is Kozma and Nitzan's Conjecture 3, posed in 2024 and open at the time of writing. The repository is explicit about what is not claimed: their Conjectures 1, 2 and 4, anything about slabs, site percolation or other lattices, and continuity of the percolation probability as a formal statement. No competing claim on Conjecture 3 was found in the four registries or on arXiv.

The artifact is not published where it says it is, and that is the first thing to check before citing it. The percolation directory does not exist on the main branch of anthropics/formal-math, whose project table lists only the zeta23 formalization; no branch carries it and the repository's own commit history for that path is empty. It survives only at the pinned commit recorded in the sources here, and the README's own repository link and AUDIT.md both point at a main-branch path that now returns 404. Verification is graded claimed rather than formal despite a passing comparator run, for two reasons: no human has read it, and the statement fidelity question is load-bearing here in a way it is not for a formalization of a known theorem. The README says so itself, that the work 'has not yet been refereed by human mathematicians or by anyone independent of the author; the only review so far was carried out by AI systems', and that readers should check that Challenge.lean states the intended theorem. There is no registration at Palomar. Autonomy is ai-led on the repository's own wording, that the Lean was written by an AI system 'working autonomously under the direction of Justin Leder; no human wrote or edited the Lean code': the direction is human, so the strictest defensible reading is not autonomous.

The improvement is stated against a specific numerical baseline, the previously known bound of 2/9 for the same limit inferior, so the delta is explicit. The note names its own predecessor, arXiv:2608.12887, and reuses that framework, which makes clear what is new here as against what was already built. No stronger bound appears in the cited literature or in the vibemathed record.

A short preprint, unrefereed, not formalized, with no independent check on record, and vibemathed records the resolution as partial. Autonomy is graded ai-led on the paper's declaration on the use of AI, which credits the model with the proof but the framework to the author: starting from the constant-twist pants decomposition approach described in the note, GPT-5.6 Sol developed the first complete proof of the main theorem through an extended discussion with the author.

The question is a clean yes-or-no about a standard construction relating Heyting algebras to elementary toposes, and the paper answers it with a specific named algebra rather than an abstract obstruction, which makes the counterexample checkable. vibemathed records no attributed poser or year, so the entry carries no year_posed rather than guessing one. No prior negative answer appears in the categorical logic literature cited.

A short preprint, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-assisted, the weakest reading the disclosure supports, because the paper claims help rather than authorship of the ideas: the mathematical results in the document were obtained with the help of ChatGPT 5.6 Sol, although the document itself was written entirely by the authors, who take full responsibility for its contents. The disclosure does not separate which results came from the model.

The target is not a named conjecture but an assumption in circulation, which the paper identifies as appearing in several articles by the authors themselves among others, so the thing being corrected is stated before it is refuted. The counterexample is at the smallest possible size, two qubits, where Wootters' formula gives the entanglement of formation in closed form and the claim can therefore be checked directly rather than argued asymptotically. No prior counterexample appears.

A short preprint, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-assisted, the weakest reading the disclosures support, because every mention of the model in the paper is of assistance in a search step inside a human-built argument: the authors use Wootters' formula and the help of Claude Fable 5 to find a state where the property fails, note that this is done very quickly with the model, and attribute one crucial corollary to work obtained with its help. The equivalence with Lipschitz lower semicontinuity, which is what makes the search possible, is the authors' own.

The question is a named one in classical function theory, stated by Nevanlinna and described in the paper's own abstract as open for over a century, with the Blaschke condition and bounded type both standard notions carrying their own literature. The paper devotes a subsection to chronology and priority, which fixes what it believes was known when. No prior counterexample appears. The result is a new construction rather than a retrieval.

A preprint days old at entry, unrefereed and not formalized, and no independent check is recorded. Autonomy graded ai-led on an unusually specific disclosure, which the paper puts in a numbered subsection headed Declaration of AI usage rather than in a footnote: the core mathematical construction and proof were generated during an autonomous run of GPT-5.6 Sol on OpenAI's ultra setting, the run lasted 7 hours 14 minutes and 14 seconds, the candidate proof was then subjected to human checking, mathematical auditing and revision, and the initial draft of the manuscript was also machine-generated and lightly revised. Graded ai-led rather than autonomous because the problem was posed and the output audited by the seven authors; the run itself is described as autonomous, and that distinction is the whole of the difference.

The target is Jerrum's long-standing question about the colouring threshold, and the paper situates itself explicitly against the recent chain it builds on: the Bochner-Bakry-Emery proof of the spectral-gap criterion of Chen, Chen, Chen, Yin and Zhang, and the trickle-down and spectral independence literature it names. The girth-five restriction is stated as a hypothesis rather than removed, so the claim is a partial advance on a known frontier and is positioned as such. No prior result at this threshold under these hypotheses appears.

A preprint days old at entry, unrefereed, not formalized, and with no independent check on record. The result is partial: girth at least five and a large maximum degree are genuine hypotheses, not technicalities. Autonomy is graded collaborative on the authors' own narrative, which describes several rounds of interaction rather than a single handoff: they first asked the model to redo known proofs by the Bochner identity, then brought it the open question, at which point it proposed an affirmative proof strategy; the human authors then verified the argument, generalized the proof with further assistance, and streamlined the paper.

Off-diagonal Ramsey lower bounds are a well-tracked ladder and the paper states the prior explicit bound it improves on, crediting Alon and Pudlak, and cites the recent off-diagonal literature it sits in. No registry carried this result at entry: it does not appear in vibemathed, MathDB, Palomar or ProofAtlas, and it reached this registry through a comment on the r/math weekly thread rather than through any catalogue. The construction is new; the p-rank framing it starts from is the authors' own and is credited as such.

A preprint, unrefereed and not formalized. Autonomy graded ai-assisted, which is what the disclosure supports and no more: the authors state that they had the idea to use p-rank arguments as the starting point, that the first construction and a bound on its clique number were provided by ChatGPT 5.6, and that they subsequently developed, refined and independently verified all arguments and take full responsibility. The model supplied one object inside a human-chosen frame, and the published construction is not the one it returned. Worth recording that the disclosure is a clearly headed AI Declaration at the end of the introduction rather than a remark buried in the body, which is better practice than several other entries here.

Erdős Problem #4 is tracked at erdosproblems.com/4 and carries a $10,000 prize; the prize question itself was settled in 2016 and the record bound since is Ford, Green, Konyagin, Maynard and Tao (2018). Green, who holds that record, read the manuscript and compared the new sieve against Erdős-Rankin (1938) directly, which fixes both what was known and what is added. No intervening record appears in the erdosproblems.com record for the problem or in the vibemathed entry. The result is a new construction, not a retrieval.

The manuscript has no human author: its title block and PDF metadata both name GPT 5.6 Sol, there is no acknowledgements section, and no human is credited anywhere in it. That is the argument for grading autonomy as autonomous; ai-led is taken instead because a human posed the problem, iterated on the output and asked for the argument to be made self-contained, and the weaker grade wins when the reading is arguable. The submitter, who is pseudonymous and wishes to stay so, states plainly that the mathematics was not theirs: 'I am not familiar with sieve theory.' Verification rests on Green becoming, in his own words, more or less convinced the argument is correct after consulting Tao and Maynard; that is expert reading, not refereeing. One attribution discrepancy is recorded rather than smoothed over: the manuscript says GPT 5.6 Sol, while the erdosproblems.com claim was filed as GPT 5.6 Pro. Boris Alexeev's Lean development transcribes the manuscript downstream rather than producing it, and this registry has not confirmed that it builds, so the grade stays at independent rather than formal. Readers on the r/math thread note that several later sections reproduce the 2018 paper with no new content, and Green calls the exposition horrific.

Convex body domination was introduced by Nazarov, Petermichl, Treil and Volberg, whom vibemathed records as posing the question in 2017, and sparse domination is a standard tool with its own literature, cited in the paper alongside the Bellman-function and sparse-revolution surveys. The implication between the two notions is what was open; the paper proves it in both the fixed-lattice and arbitrary-cube settings rather than one. No prior proof of the implication appears.

A short preprint, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-assisted, the weakest reading consistent with the disclosure, because the paper's AI disclosure statement claims only prototyping and not discovery: GPT-5.6 Sol Pro, accessed through ChatGPT, was used to prototype proof strategies for this note. Nothing in the disclosure attributes the final argument to the model.

The prior state is unusually clean here because it is the authors' own: the implications from frequency interpretation to generic stability of the random extension to self-averaging were established in their previous work for discrete theories, and the reverse implications are what remained. The paper states that division explicitly, so what is new is not in doubt. No competing proof of the reverse implications appears.

A preprint, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-led on the paper's AI acknowledgment, which reports both discovery and cross-checking by several models followed by substantial human rewriting: a proof of the main theorem was initially obtained from a ChatGPT 5.5 query focused on the discrete case, the authors were also able to find proofs independently using Kimi K3 and Claude Fable 5, and the arguments were then heavily reorganized and rewritten by the authors with further assistance from ChatGPT 5.6 Sol.

The paper states exactly which generator-count ranges were already covered and by what, the classical cases r at most 5 and the Boij-Dannetun-Lundqvist equal-degree theorem through degree d + 2, and therefore which ranges required new input. That makes the contribution a bounded and stated delta rather than a broad claim on Fröberg's conjecture, which remains open in general. No prior treatment of these ranges appears.

A preprint, unrefereed, with no independent check on record, and vibemathed records the resolution as partial: this is two degrees in four variables, not Fröberg's conjecture. The certificates are explicit and the nonzero-modulo-2 minors make the endpoint computations checkable, but nothing is machine-checked, so the grade stays at author-verified. Autonomy is graded collaborative on a broad disclosure of automated assistance that spans the whole pipeline without separating human from model contribution: the workflow used GPT-5.6 Sol, Claude Fable 5 and Grok 4.6 for the formulation of mathematical ideas, generation of conjectures and proof strategies, derivation and checking of intermediate steps, construction of examples and exact certificates, comparison of literature and candidate proof approaches, and organization of arguments.

The question and its partial answer are both named, dated and cited: Massey posed it in 1978 and Ancheta settled the p = 1/2 case that same year, so what remained was every other bias. The note also records, as a correction to its own novelty, that a literature search aided by Codex found several proof ingredients already present in or deducible from prior work, and devotes a section to that discussion. That is a partial-novelty flag surfaced by the author rather than by a later reader.

A short preprint, unrefereed, not formalized, with no independent check on record. The novelty is qualified by the author's own hindsight statement that several ingredients of the proof have appeared in, or can be deduced from, the prior literature, discussed in the note's Section 4.1; what is claimed as new is the extension itself and a simplified self-contained presentation. Autonomy is graded ai-led on the declaration of AI use, which credits discovery to the model and simplification to the author: the first version of the proof was discovered by GPT-5.6 Sol in an interactive process guided by the author, who subsequently simplified the program and developed the self-contained proof presented in the note.

The problem is named, ancient and heavily attempted: Hopf posed it in 1948, and the modern literature runs through Chern, Bryant, LeBrun and the Campana-Demailly-Peternell papers the manuscript cites and disputes. Its 60-item bibliography is real and checkable. The specific construction, a family of 2-tori over the (3,4,infinity) orbifold completed at its three special points, does not appear in the prior literature, and no accepted complex structure on the six-sphere exists. Atiyah's 2016 attempt is the best-known recent failure and is not this argument. The construction is new; whether it is correct is a separate question this entry does not settle.

Enters at claimed, and there are three separate reasons not to grade it higher. First, the AI attribution rests on a social-media post and nothing else. The 108-page manuscript was read here in full: it has no acknowledgements section, no methods note and no mention of Claude, Anthropic or any paraphrase anywhere in its text. The author's public post names the model and credits it substantively, but says nothing about which parts of the work it did, and no stable direct link to that post could be confirmed. Autonomy is graded ai-assisted because that is all the disclosure can carry, not because the contribution is known to be small. The model version is not stated. Second, the result contradicts a published theorem. The paper carries a section headed on why the argument of the Campana-Demailly-Peternell corrigendum does not apply, and a remark stating that its theorem contradicts that paper's Corollary 2.3 as published, locating the divergence in a non-vanishing higher direct image and in a lemma there that assumes trivial monodromy where here the monodromy is non-trivial. Worth reading both ways: the 1998 paper's Lemma 1.5 was itself wrong and the 2020 paper is the corrigendum, so that literature is known to be fragile, which makes the collision survivable without making the claim likelier. Third, the problem has a long history of false proofs. Not peer-reviewed, not formalized, and no independent check is recorded.

The rank record ladder is well documented and tabulated by Dujella, which makes the prior state of the art unambiguous: Elkies rank at least 28 in 2006 and Elkies and Klagsbrun rank at least 29 in 2024. Both new curves are given explicitly with their a-invariants, conductor, discriminant and regulator, so the claim is checkable against that table rather than resting on an assertion. No intervening record appears. These are new curves, not a rediscovery.

Recorded only as leaderboard database entries: there is no preprint, no transcript and no refereeing, and nothing is formalized. The two records are kept in one entry because they are the same method and the same people four days apart. Independence of the points is asserted through the leaderboard's stated general practice of exact 2-descent rather than reproduced on the page, and the exact-rank claim is conditional on BSD and GRH with no numeric derivation published for either curve. What the model contributed is documented only by the leaderboard's own commentary field, which reads in full: 'BSD + GRH certified to rank 31, found by Claude, Levent Alpöge, and Ava Howell.' Autonomy is graded ai-assisted on that thin evidence, because the search framework is the humans' and no stronger reading is defensible. Neither record answers the open question of whether ranks are unbounded.

Two pieces of prior work bound what is left to prove, and both are recorded in the repository rather than found later. Problem 270 as Erdős and Graham posed it, for every f tending to infinity, was already answered in the negative by Crmarić and Kovac in 2025, who showed some such f makes the series sum to any prescribed value; what survives is the non-decreasing case, inside which the affine family sits. Separately, the short irrationality proof for the base constant is Crmarić and Kovac's, posted by Kovac on the Erdős Problems forum in July 2026 and credited in the repository, and base-case transcendence follows from known results. So the checkable parts were already known and the new content is the affine extension.

Announced through a repository rather than a paper, unrefereed, with no independent check on record, and vibemathed lists it as a candidate pending review. The Lean development is explicitly partial: the repository separates what is fully verified from what is not yet verified, so the transcendence claim as a whole is not machine-checked and the grade stays at claimed. The novelty is narrow for the reason given above, since the pieces a reader can most easily check are the ones already in the literature. Autonomy is graded ai-led on the repository's own AI disclosure, which is unusually sweeping: generative AI performed nearly all of the mathematical work, independently rediscovering the elementary denominator argument, developing the affine extensions and the transcendence-theoretic arguments, conducting the literature search, writing the manuscript and producing the Lean formalization, with the repository owner directing and supervising. No human author is named on the work.

Dubickas posed the question as Problem 3 of his 2006 Glasgow Mathematical Journal paper (48, 331-336), and it is stated as open there and in the subsequent Z-number literature descending from Mahler. The neighbouring case alpha equal to 3/2 is Mahler's problem and remains open, which fixes the boundary of what is claimed here. No prior resolution of Problem 3 appears. The result is new, and the paper also generalizes past the original question rather than only answering it.

The Lean covers less than the paper. The author states that the case m equal to 3 is what is machine-verified, and the repository flags the thickness computation of section 4.1 and the whole of section 8 as not formalized, so the formal grade attaches to the central claim rather than to every theorem in the write-up. Not peer-reviewed. Autonomy graded ai-led on an unusually explicit disclosure: the author records that the mathematical discovery is the Fable 5 agent's, that the formalization is the Fable 5 and Opus 5 agents', that the agents drafted the prose which the author revised, and that the direction, review and responsibility are the author's. The Lean development carries the same framing in its copyright line.

The question is attributed to Heuer and Loh and dated 2019 in the vibemathed record, and the counterexample is a pair of concrete words whose properties can be checked directly rather than an existence argument. The repository accompanying the paper reproduces the computation, so both halves of the claim, the isomorphism and the difference in stable commutator length, are independently re-runnable in principle. No prior counterexample appears.

A short preprint, unrefereed, with no independent check on record. The formalization is partial and does not cover the result: the repository contains a Lean formalisation of the six identities used in the argument, produced with the assistance of Harmonic's Aristotle, not of the full claim, so the grade stays at author-verified rather than formal. Autonomy is graded ai-assisted, the weaker of the two readings the paper's own wording admits, since the body says Claude Desktop with Opus 5 designed and orchestrated an exhaustive search through orbits of words of bounded length while the acknowledgement says it assisted in designing and orchestrating that search.

The question is recent and attributed: Boucksom, Guedj and Lu posed it in 2025, so the window in which a prior answer could exist is short and the paper names the source directly. The counterexample is a single named manifold, the Hopf threefold, rather than an abstract existence claim, which makes it checkable against the definition. No prior counterexample or positive resolution appears.

A short preprint, unrefereed, not formalized, with no independent check on record. Autonomy is graded ai-led on a one-sentence disclosure that credits the construction itself to an agent rather than to assistance: the initial counterexample was constructed with the Rethlas agent, improved by Felix Ye, using the gpt-5.6-sol model. The disclosure covers the initial counterexample only and does not say how much of the final write-up is the authors' own.

Marton posed the inner bound in 1979 and its tightness is the standing open problem of broadcast-channel capacity, restated in the network information theory literature and in the Gohari-Liu-Nair line of work the paper builds on and partly refutes. The paper records that the Markovity conjecture had survived an experiment over more than ten thousand random channels in earlier work, which fixes the prior state of the art: no counterexample to either conjecture had been found. No prior demonstration of sub-optimality appears. The result is a new construction rather than a retrieval.

A preprint one day old at entry, unrefereed and not formalized. The gaps are of order ten to the minus six, so the claim rests on the authors' interval-arithmetic certification rather than on anything visible by inspection, and no independent rerun is recorded. Autonomy graded ai-assisted rather than collaborative or ai-led: the acknowledgement credits each contribution individually and the recurring verb is assisted. Chandra Nair asked Yanxiao Liu to search using AI; GPT-5.6 Sol assisted Liu to a Markovity counterexample and, independently, assisted Mian Huang via the human-devised method of elimination geometry; Claude Fable 5 assisted the tensorization test; Claude Fable 5 and Opus 5 assisted a fixed-input-distribution example after Amin Gohari and Nair suggested that constraint; and Yanxiao Liu then modified that example into the unconstrained counterexample. Humans chose the method, set each search target and did the final construction. The weaker defensible reading applies.

The paper positions itself against Arnold's fast-dynamo problem and the dynamo literature it cites, and the arXiv comment records the provenance directly as AI discovered, human written. vibemathed records the resolution as a variant rather than the original problem, which is the honest reading: what is built is a smooth random field with the growth property, not a resolution of the fast-dynamo problem as classically posed. No prior construction of this kind appears in the cited literature.

A preprint, unrefereed, not formalized, with no independent check on record, and a variant of the classical problem rather than the problem itself. Autonomy is graded ai-led on an explicit disclosure: the author writes that the central proof idea was generated essentially autonomously by ChatGPT 5.6 Sol Ultra from a prompt adapted from an earlier preprint, and that the manuscript was written and verified by the author. Some simplifications over the machine-generated manuscript are the author's, including a simpler set of velocity fields and a more direct iteration argument, and the model was also used to explain sections of the original argument back to the author and to copy-edit.

The conjecture is pinned to a specific numbered statement in a specific published paper, Conjecture 13 of King, Gosset, Kothari and Babbush in PRX Quantum 6, 010336 (2025), which leaves no ambiguity about what is being refuted or when it was posed. The consequence that fails with it, a triply efficient algorithm for arbitrary Pauli subsets, is stated in the same source. No prior counterexample appears.

A preprint, unrefereed, not formalized, with no independent check on record, and vibemathed lists it as a candidate pending review. Autonomy is graded collaborative rather than ai-led because the disclosure is a single sentence with no account of the division of labour between the model and the three authors, and the weaker grade wins when the reading is arguable. The sentence, in full, is: GPT Sol 5.6 was used to derive the main results (Theorem A and Theorem B) of this paper.

The conjecture is named, celebrated and traceable: the paper states it as Donaldson's 2002 conjecture, records the normality repair of the original scheme-theoretic formulation due to Ross and Thomas, and cites the Matsushima and Futaki obstructions and the Chen-Cheng and Berman-Darvas-Sjöström Dinew lines of work as the surrounding literature. No prior counterexample in any dimension appears. The paper is explicit about what was and was not already available: candidate manifolds of the present shape date to 2008, and what was missing is the proof that the mechanism works. The result is new.

A preprint days old at entry, 79 pages, unrefereed and not formalized, and a counterexample of the kind that cannot be checked by evaluating an object, so verification means reading the classification argument. The theorem actually proved is the extremal-metric statement, which is stronger than the cscK wording of the abstract. Autonomy graded collaborative rather than ai-led: the appendix says the author found initial signs of a breakthrough while exploring open problems with Claude Code and then had Claude Code, Codex and Danus work on it in collaboration, with the three systems together producing the counterexample and its proof, but it also records that human input was crucial at one point, when the author recognized the example had to refute either the Codogni-Stoppa conjecture or cscK Yau–Tian–Donaldson and directed the agents to settle which. The appendix further reports that an improved version of Danus, given only the original problem and none of the earlier findings, later settled it alone in 5 hours and 29 minutes without that human input, which would be autonomous; that system is not public and the report is by the same author, so it is not gradeable evidence. The weaker defensible reading applies.

Carathéodory's conjecture is a named problem with a long literature and a standing partial theorem, Hamburger's real-analytic case from 1940-41, and it appears as Problem 8.1 in Ghomi's published problem list. The claim is a counterexample in the smooth category only, which is consistent with rather than contradicting Hamburger. No prior smooth counterexample appears in the problem list or in the vibemathed record. The construction is new work, not a retrieval of something already in the literature.

Announced in an X post rather than a preprint, and unrefereed. The Lean formalization is sorry-free at a commit but not merged, and vibemathed records its statement as read rather than compiled and audited, so nothing here is machine-checked end to end for this registry's purposes; the grade stays at claimed. Autonomy is graded ai-assisted rather than higher on a deliberately strict reading of two separate model roles, neither of which is the discovery: Alpöge's announcement credits John-Paul Smith and Claude with checking the construction, which makes the model a verifier of a human construction, and the Lean development was, in its author's words, developed with Codex and parallel proof-review agents, which is formalization of a human result. Only the smooth case falls; the classical real-analytic form of the conjecture remains true.

The conjecture is named and dated to Kára, Pór and Wood in 2005, and the paper identifies l = 4, k = 6 as the first case left open by the existing partial results, which fixes the prior state of the art. The threshold is explicit, so the statement is falsifiable as written rather than asymptotic hand-waving. No prior proof of this case appears in the discrete geometry literature or in the vibemathed record.

A short preprint, unrefereed, not formalized, with no independent check on record, and vibemathed lists it as a candidate pending review. The threshold is astronomically large and the result settles one case rather than the conjecture. Autonomy is graded ai-led on the paper's own AI disclosure, which is unusually specific about the sequence: after one fruitless attempt and what the author calls the now customary generic encouragement, a relatively detailed proof of Theorem 1 was provided by GPT-5.6 Sol Pro after pondering for 222 minutes.

The question is attributed to a specific venue and date, Koivisto at Dagstuhl 2013, and the 2^n barrier for the general problem is the standing baseline the paper names. The refinement is stated against a specific prior argument, Kozma's for two-dimensional posets, which makes the delta explicit. A verification script ships as an ancillary file with the preprint. No prior sub-2^n algorithm for the general problem appears.

A preprint, unrefereed, with no independent check on record, and vibemathed lists it as a candidate pending review; the ancillary verification script is not a proof artifact and nothing is formalized. Autonomy is graded ai-led on an unusually layered disclosure: the core mathematical ideas behind the new part of the algorithm and proof are stated to have been discovered by Claude Opus 5, while the research prompt supplied to it was itself generated by ChatGPT 5.6 Sol, which the author instructed to model the prompt on OpenAI's publicly released one for the cycle double cover work, so the prompt-generation stage was AI-assisted as well. Generative tools were also used for literature search, drafting and verification assistance.

The problem is tracked at erdosproblems.com/501 and traced in the repository to Erdős 1961, Problem II.9 and Erdős-Hajnal 1971. The repository checks its own novelty claim against the database directly: in a snapshot of teorth/erdosproblems dated 2026-08-17 covering 1217 problems, the problems already marked independent, not provable or not disprovable all carry formal_status unformalized, while #501 is listed as open. That is the basis for the repository's claim that this is the first Erdős problem whose resolution is a formally verified independence result. The second question was settled by Newelski, Pawlikowski and Seredyński in 1987 and is formalized here without the boundedness hypothesis.

Announced through a repository rather than a paper, and unrefereed. The credit is shared and mostly human, which is why autonomy is graded collaborative rather than higher: Hechler supplied one direction in 1972, Newelski, Pawlikowski and Seredyński settled the second question in 1987, Sungchul Lee derived a positive answer from a real-valued measurable cardinal with assistance from GPT-5.5 Pro, and Nat Sothanaphan observed that the two halves together give independence. What Glazer and Sol added is the removal of the large cardinal assumption. The formal grade covers the Lean development, which builds under CI and proves its targets from the standard axioms; the Lean statements have not been audited by a third party against the informal problem, beyond the repository's own faithfulness target.

The conjecture is named, attributed to DeLaViña and Waller and dated 2008 in the vibemathed record, which is where this candidate is carried. The claim is sharpened rather than merely asserted, since the equality cases are enumerated and include two sporadic small-diameter graphs alongside the cycle, and those exceptions are the sort of detail a re-derivation can check. No prior proof appears in that record.

A Zenodo preprint, unrefereed, not formalized, with no independent check on record, and vibemathed lists it as a candidate pending review with a low significance rating. The Zenodo metadata carries no abstract, so the statement here is reconstructed from the registry record rather than from the deposit's own description, and a reader should open the deposit before relying on it. Autonomy is graded ai-assisted on the only account of the model's role available, which is the registry's one-line summary that the models assisted in developing proof strategies and checking computations; no AI disclosure written by the author has been located.

The conjecture was proposed at the NSUCRYPTO 2019 cryptographic olympiad, with the proposer not publicly disclosed, and the companion repository supplied with the problem records which supporting facts were already formally verified, so the starting point is unusually well defined. Working from that inventory the authors identify one hypothesis in it as essential and correct it, which is itself evidence the prior material was checked rather than assumed. The result is a partial proof of an open conjecture, not a retrieval.

A preprint, unrefereed, with no independent human check on record, and the result is explicitly partial: four residue classes of k modulo n plus exhaustive verification for n at most 13, not the conjecture. The formal grade rests on the authors' statement that all new results and proofs have been formally verified in Lean 4 by Aristotle from Harmonic, with provenance details in the acknowledgements; vibemathed records the Lean development as checked with its statement unaudited, so nobody outside has confirmed the formalized statements match the paper. Autonomy is graded ai-led on a strong and specific disclosure: every proof in the paper was obtained by prompting Claude Fable 5 with the conjecture statement, background hints and a pointer to the companion repository, and the human authors supplied the framing and the subsequent verification.

The theorem is not new and the project does not claim it is. H at most 246 is Polymath8b, 2014, building on Maynard 2013 and Zhang 2013, and all three are cited by the project as the sources being formalized. What did not previously exist is a machine-checked proof: no formalization of the Maynard sieve or the Polymath8b bound appears in Mathlib or in the Lean community's project index before this, and the related PrimeNumberTheoremAnd project it builds on formalizes a different theorem. This entry records a formalization milestone, in the same sense as the strong prime number theorem entry, not a new mathematical result.

The formalization is not self-contained. Palomar registered the development under the theorem names bombieriVinogradov_implies_prime_gap_le_246 and bombieriVinogradov_implies_nth_prime_gap_le_246, and Palomar's own record describes the flagship result as conditional on the Bombieri-Vinogradov theorem, which is assumed as a hypothesis because it is not yet in Mathlib. Bombieri-Vinogradov has been a theorem since 1965, so the mathematics is unconditional in the literature and only the Lean development is conditional, but the project's public page states the 246 result without that qualification, and the two readings should not be conflated. Beyond the mechanical Palomar check there has been no mathematical peer review of the formalization choices. Autonomy graded collaborative: the disclosure is that the proof was generated collaboratively between human formalisers and AxiomProver, with humans curating and librarizing, and roughly 41 named contributors are credited.

Stein posed the question at the 1986 ICM and the paper cites it directly, along with the authors' own 2021 Communications in Contemporary Mathematics paper on the dimensional weak-type (1,1) bound, which fixes the prior state of the art as dimensional rather than dimension-free. Dimension-free strong-type bounds are long established and are not what is claimed here. No prior dimension-free weak-type constant appears in the literature. The result is new.

A preprint, unrefereed and not formalized, with no independent check recorded. Autonomy graded collaborative rather than ai-led, and the disclosure is detailed enough to justify the weaker reading: the statement opens by saying the proof strategy was developed by large language models in dialogue with the authors, but the same paragraph records that the first attempt failed and produced only partial results, that a second attempt yielded a solution the authors judged significantly more complicated than what was published, that the human authors then assessed feasibility and redirected the work into Euclidean space, and that they checked and rewrote the proofs where the presentation was unnatural, performed the literature review, and take full responsibility. Humans chose the route that was kept. The weaker defensible reading applies.

The exponent has a well-tracked ladder of published upper bounds running through Duan, Wu and Zhou (2022), Vassilevska Williams, Xu, Xu and Zhou (2024) and Alman, Duan, Vassilevska Williams, Xu, Xu and Zhou (2025), and the paper states the prior best as 2.371339 and cites it. No lower published upper bound appears before this note. The result is a new bound rather than a retrieval, and it is an improvement of roughly 1.6 times ten to the minus four, which the authors themselves describe as a small step.

A preprint, unrefereed at entry. A bound of this kind is not the sort of claim a reader can spot-check: the number falls out of a large optimization over laser-method parameters, so reproducing it means re-running the optimization rather than checking a certificate, and no such independent rerun is recorded. Autonomy graded search-scaffold, consistent with the other AlphaEvolve entries here: AlphaEvolve is a human-built evolutionary harness with a language model inside, and in this paper it is the last stage of a pipeline whose first two stages are ordinary human applied mathematics. The author list mixes the DeepMind team with the complexity theorists who set the previous record, which is where the reformulation comes from.

Talagrand posed the hypercube conjecture in 1989 and it remained on O'Donnell's open-problem list; even the Gaussian special case was open as of 2012. The prior state of the art is fixed precisely by Chen, arXiv:2511.19374, November 2025, which proves the bound up to a log log correction and says so in its title. This paper's stated contribution is the removal of exactly that factor, and the mechanism it credits, a fixed-numerator frozen exponent that dispenses with the growing stopping buffer, is specific to the gap. The result is one step in a chain rather than a proof from scratch, and it is new.

A preprint days old at entry, unrefereed, not formalized, and with no independent endorsement recorded. The AI disclosure is two sentences, in the abstract and again under a heading 'The role of AI in this proof': the Odin Automatic AI Research Agent was used to discover the proof, and the final proofs were reorganized by the authors. Autonomy graded ai-led on that statement taken at face value, but the claim cannot be audited: Odin is not a publicly documented system, no vendor is named, no transcript or artifact is published, and there is no way to separate discovery from reorganization. Read the model field as the authors' attribution rather than as a verified fact.

The question is one of the two 2004 Džamonja–Shelah questions that organised two decades of classification theory, and the paper's own introduction traces it as open through Mutchnik's celebrated resolution of the other half and the partial results that followed. It is repeatedly highlighted in the NSOP_1 literature as the surviving open case. No prior proof appears. The result is new.

A preprint one day old at entry, not peer-reviewed and not formalized. The acknowledgements record comments from Itay Kaplan and Scott Mutchnik on a preliminary version, which is expert attention on a draft rather than independent verification, so the entry stays at author verified. Autonomy graded collaborative: the entire disclosure is one sentence, that the proof was found using ChatGPT 5.6 and simplified and streamlined by the author, which is ambiguous between the model supplying the key insight and the author using it as a tool. The weaker defensible reading applies.

The conjecture is a named 1932 problem of Banach with a documented partial-results ladder: Gromov's theorem covers even n, and subsequent work settled particular odd dimensions, which is the prior state of the art the paper states and cites. Searched arXiv and MathSciNet for a proof covering all odd n; none appears before this preprint, and the surveys of the problem still list the general odd case as open. The result is a new proof rather than a retrieval.

A preprint, unrefereed and not formalized, and only days old at entry. Autonomy graded ai-assisted rather than collaborative: the declaration states that the authors had already reduced the main problem to proving Theorem 3.10 before using generative AI, that an approach to that theorem then emerged through extensive interactions with ChatGPT 5.5 Pro and 5.6 Pro, that GPT-5.6 Sol generated the initial draft of Section 3 and corresponding material in Section 2, and that the authors checked and rewrote it and take full responsibility. The reduction, which is the framing step, is human, and the machine contribution is one theorem inside it. The weaker defensible reading applies.

The sharp threshold is the tracked open problem of the liquid drop literature, followed across calculus of variations, mathematical physics and geometric analysis, with a 2017 Notices of the AMS survey and partial results carrying Lieb, Otto, Figalli and Maggi. The prior state of the art is stated in the paper and checks out: minimality of the ball was known only up to volume 1 (Chodosh–Ruohoniemi, CPAM 2025) and nonexistence only from volume 7.5 upward (Schulz, arXiv:2608.09000, posted two days earlier), leaving the interval from 1 to 7.5 open. Frank and Nam had proved existence up to the threshold in 2021, and the new proof uses that result rather than superseding it. Uniqueness across the whole range and nonexistence immediately above the threshold are new.

A preprint, not peer-reviewed, with no formalization. Verification is author-side: the authors state they checked and reworked the proof, which is not independent replication. Autonomy graded ai-led on the paper's own disclosure, which says the results were obtained by ChatGPT 5.6 Pro over a series of chats without significant assistance from the authors and that the fundamental strategy remains close to the model's original output; the authors checked the proof, reworked it and wrote the manuscript, and state the article contains no AI-written text.

The question is stated by Bekos, Kaufmann and Pfister about the earlier book-embedding algorithm of Alam and co-authors, and the paper answers it directly rather than a nearby question. Searched for a prior counterexample to prescribed-cycle recovery and none appears; the surrounding literature treats the recovery question as open. The construction is a new explicit instance, not a retrieval. Barnette's conjecture itself is untouched and remains open, so nothing in the novelty claim depends on it.

The formalization is partial by its own account: the Lean covers the finite combinatorial core, and the topological realization of the incidence data as a sphere embedding, together with the published algorithm's Property 1, remain external inputs. So the machine checking establishes that the displayed graph has the stated combinatorial properties and that the obstruction fires, not the whole argument end to end. Not peer-reviewed. Autonomy graded ai-assisted on the paper's own disclosure, which is the authoritative one: Codex assisted with literature and novelty searches, certificate verification, code testing, proof development, and manuscript drafting and editing, while Claude was used for independent adversarial review, and the author states that neither system qualifies as an author and takes full responsibility. Worth recording a discrepancy: the Palomar record lists the authors as the human plus two model names, which the paper explicitly declines to do. The paper's statement is the one graded here.

The proportion ladder is a documented literature running from Hardy (1914) and Selberg (1942) through Levinson's one third (1974) and Conrey's two fifths (1989), with subsequent refinements reaching about 41.6%; the paper states the prior record and cites it. The model itself searched 54 arXiv papers for prior art before write-up. No earlier unconditional bound above 42% appears in the literature. The result is a new bound, not a retrieval of a known one.

Not peer-reviewed. The Riemann hypothesis itself is untouched, and Anthropic states it does not expect these techniques to lead to a proof of it. The Lean formalization is sorry-free and anchors its statements on Mathlib's own riemannZeta and analyticOrderAt with the corresponding counting functions rather than an assumed form of the result, which is real statement anchoring; but the assembly of those primitives into the proportion claim is the paper's own, and that assembly is exactly what nobody independent has audited. The same organisation produced both the proof and its formalization. Two Anthropic mathematicians studied and validated the work, which is author-side review, not independent replication. Autonomy graded ai-led rather than autonomous: humans posed the problem, supplied the environment and validated the output.

The Petersen coloring conjecture is tracked as open in the Open Problem Garden, whose entry calls it an extraordinary conjecture, and it carries a substantial literature on normal edge-colorings and sublinear approximations built on the assumption that it holds. No prior counterexample appears anywhere in that literature. The construction is a new concrete graph, not a retrieval of an existing example.

A preprint, not peer-reviewed. The paper's computational provenance section states only that OpenAI language-model systems were used extensively in the discovery, computational search, verification and preparation of the work, and names no product, version or division of labour, so the model field records an unnamed OpenAI system and autonomy is graded ai-assisted, the weakest reading the disclosure permits. The paper does not claim 112 is the minimum order for a counterexample.

The separation question between ordinary and strong Kreiss constants is attributed by vibemathed to Chalmoukis and Tsikalas and dated 2025, so the window for a prior answer is short. The inverse generator problem is the older and better-known target, and the paper answers it in the negative on Hilbert spaces, the setting where it was sharpest. Both claims descend from one explicit finite-dimensional construction whose entries are given by explicit formulas, so the construction can be inspected directly. No prior counterexample appears.

A preprint, unrefereed, with no independent check on record; it has been revised, with v1 posted 2026-08-06 and v3 on 2026-08-26, and the date here is the first public posting. The formalization is partial and covers the finite-dimensional core rather than the claims of the entry: the proof of Theorem 1.1 has been formalized in Lean 4 in a public repository, while the semigroup and Kreiss deductions drawn from it are not machine-checked, so the grade stays at author-verified rather than formal. Autonomy is graded ai-assisted on a disclosure that keeps the model in a search and formalization role: ChatGPT 5.6 Pro was used to explore various Schauder basis counterexamples to the inverse generator problem, and the Lean 4 formalization was done using Claude Fable.

Sendov's conjecture is a named 1959 problem with its own Wikipedia article in four languages and a partial-results literature spanning 67 years. Tao's 2020 paper on the sufficiently-high-degree case (arXiv:2012.04125) states the general case as open, which fixes the prior state of the art precisely. No earlier proof covering all degrees appears in the literature, and the Phelps–Rodriguez corollary is new with it. The result is a new proof, not a retrieval. On priority between the two formalizations: Palomar's record for Tao's development notes that it shares no code with Mazur's, was written from the blog-post digestion rather than from that proof, and that priority for the first machine-checked proof of Sendov's conjecture belongs to Mazur's ProofAtlas work.

Not peer-reviewed. Mazur's own Lean package cannot be recompiled as distributed: the published bundle ships no lakefile or manifest and excludes Mathlib, so the formal grade rests on Tao's independent formalization rather than on the original artifact. Autonomy graded collaborative rather than ai-led: the disclosure credits GPT-5.6 Pro with substantial contribution to the discovery and derivation of the proof, including exploration, proof development, exact computational testing and adversarial auditing, but it also has Mazur directing the research workflow and selecting and reconciling the model's outputs, which is mathematical judgment rather than cleanup. The weaker defensible reading applies.

Schiffer's conjecture is Problem 80 on Yau's list, with a partial-results literature running since the 1970s, and the Pompeiu problem has stood since 1929. Both are recorded as open in the standard references and in DeepMind's formal-conjectures repository, which carries a Lean statement of the Pompeiu problem as an unsolved challenge that this work's formalization closes. No prior counterexample to either appears. The construction is new.

A preprint, not peer-reviewed. The Lean 4 verification was written by GPT-5.6 from an early draft of the paper and lives in an author's own repository; it had no independent audit at entry time, and the same group produced both the proof and its formalization. Autonomy graded ai-assisted: the paper is explicit that the novel construction strategy is the authors' own, and that the models were used to verify the asymptotic estimates numerically, to produce first drafts of the proofs of the Bessel function estimates, and to help with exposition.

The degree-diameter problem is a named and long-tracked question in extremal graph theory, surveyed by Bermond and Bollobas (1981) and with Bollobas's 1978 Extremal Graph Theory as the reference point for the asymptotic question; Bachraty, Siagiova and Siran had approached the bound for diameter three in 2019. The authors note that after completing the work they learned the projective-plane construction of an earlier paper shares the rank-2 incidence graph underlying the k=1 case of theirs, and state the higher-rank construction and its odd-even routing argument are independent and different. No prior proof of the general asymptotic result appears.

Not peer-reviewed. Autonomy is graded ai-assisted, the weaker defensible reading, because the disclosure is explicit that the authors developed the suggestion into the construction, formulated and verified all mathematical arguments, and take full responsibility for the content; the model's contribution was one structural idea during brainstorming. Generative tools also assisted with the Lean formalization. The Lean repository is author-produced and had no independent audit at announcement.

Each of the ten is a named open problem with a documented origin: soficity from Gromov 1999, Connes rigidity from 1980, and the sphere-packing exponent improvement is the first on the general bound since 1978. The Lean repository states which prior bound each result improves. Thomas Bloom, who maintains erdosproblems.com and publicly corrected OpenAI's 2025 Erdős retrieval episode, called these results big news, which is meaningful given that he is the person who caught the previous overclaim.

The certificates are checkable and the claim that the theorems hold is as solid as Lean makes it. The claim about provenance is not checkable: Astra is unreleased, so no outside party can test whether the model produces these results, and the account of how they were found rests entirely on OpenAI. Grading verification as formal reflects the proofs, not the provenance; a reader who cares only about who found it should read this as claimed. Specialist review of the mathematical significance is still pending in several cases. Noam Brown noted there are no Millennium Prize problems here. Press summaries of the ten disagree with the repository's own list, some substituting specific Erdős problem numbers that do not appear in it; the list above follows the repository.

The relationship between sumset and difference-set growth is a standard question in additive combinatorics with a long record of partial bounds on the exponent; the extremal value was recorded as undetermined. The paper states the prior bounds it improves on. The construction is new, not a retrieval of a known extremal family.

A newly released arXiv v1 preprint, not peer-reviewed. The Lean 4 and Mathlib formalization is author-provided; the repository reports lake build completing with no sorry declarations or warnings, but the principal asymptotic and supremum results rely on three native_decide certificates for elementary finite computations over a 12-element base-39 digit block, so those steps are trusted to the Lean kernel's decision procedure rather than proved term by term. Autonomy graded ai-led rather than autonomous: the agent produced the construction, but humans posed the problem, checked it and wrote the final proof.

The complexity of Kemeny aggregation for three voters is a specifically tracked open case in the computational social choice literature, following Dwork, Kumar, Naor and Sivakumar's 2001 work establishing hardness for four voters and the subsequent extension to all even counts. The odd cases, and three in particular, were repeatedly noted as open. No prior hardness proof for exactly three voters appears.

Not peer-reviewed. The Lean check covers the reduction; it is author-produced and had no independent audit at announcement. Autonomy graded ai-led rather than autonomous: the model found the reduction, but the human author posed the problem, reviewed the argument and wrote the paper.

Feige's conjecture is documented as open from his 2004 paper on sums of independent random variables, where he proved the weaker constant 1/13. The sharp 1/e constant is recorded as an open problem in the subsequent small-deviation literature and had stood for 22 years. No prior proof of the sharp constant appears; the near-simultaneous arrival of three independent proofs within days confirms it was live and open, not settled and forgotten.

Not peer-reviewed; all three proofs are preprints. The Lean formalization accompanies the primary paper and is author-produced. Autonomy is graded ai-led rather than autonomous because the human authors posed the problem, then checked, revised and rewrote the argument for publication. The three independent proofs are genuine corroboration of the result, though two of the three were themselves AI-assisted, so they are not fully independent of the method.

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.

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.

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.

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.

The Kourovka Notebook is itself the authoritative open-problems register for group theory, and each of the eight is recorded there as open with a named proposer, so novelty is established by the source of record rather than by a literature search. The authors submitted solutions to the Notebook editors and the problem proposers for acceptance before publishing, and the initial submissions remain in the Notebook's own preprint repository. Problem 3.46 traces to Plotkin's survey question on products of locally soluble normal subgroups, which Baumslag, Kovács and Neumann had partly addressed in the negative.

Not peer reviewed as a journal article, though the individual solutions were accepted by the Kourovka Notebook editors and the problem proposers, which is the relevant gatekeeping for this venue. The autonomy grade rests on the authors' own disclosure: they state Aristotle developed the proof strategies without human guidance about which steps to take, while they monitored its work, intervened when clarifications were needed, and built a library of relevant concepts with it. That library work and the final canonisation for Mathlib upstreaming were done partly by hand. The Lean certificates are the load-bearing evidence and anyone can rerun them; the claim about how the arguments were found rests on the authors' account.

The Gaussian product inequality is a named conjecture dating to 2007, with a substantial partial-results literature covering special cases such as even integer exponents and small dimensions; it was recorded as open in the general case. The proof settles the general statement. No prior general proof appears in the literature.

Not peer-reviewed; released as a preprint with a public chat transcript rather than through a journal. The Lean formalization is author-produced. The AI output omitted the equality-characterization half of the strong form, which was supplied around it. Checks by other models (ChatGPT 5.6 Sol Pro, Gemini 3.1 Pro, Grok 4.5) are not independent human verification and do not raise the grade; the human check by Ouimet is author-side.

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.

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.

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.

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.

Sabidussi's compatibility conjecture is a named open problem in graph theory concerning eulerian trails and compatible circuit decompositions, with a partial-results literature covering restricted degree conditions. It was recorded as open in the general case. No prior general proof appears.

Not peer-reviewed. The Lean formalization is in the author's own repository and had no independent audit at announcement. Autonomy graded collaborative rather than ai-led: the source describes the proof as developed with the models and reviewed by the author, without attributing the key idea specifically to the model, so the weaker defensible reading applies.

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.

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.

The conjecture is recorded as open in the standard references, including Wolfram MathWorld, and has a documented history of proof claims posted to arXiv that were later withdrawn or found to have gaps, so the prior state was unambiguously unresolved. One thing complicates the picture rather than the novelty: Shiva Kintali posted an independent Codex-assisted proof claim of the same statement three days later (arXiv:2607.14140), also routed through nowhere-zero three-bit flows and likewise unreviewed. The result is a new proof, not a retrieval of a known one.

Not peer-reviewed. The conjecture's history of gapped proof claims is itself a reason for caution, and mathematicians are treating this one as unconfirmed pending expert review. The Lean development does check the unconditional statement for finite loopless bridgeless multigraphs, sorry-free and admit-free with no project-specific axioms, but it is first-party, produced by the same organisation as the proof, and had no independent audit at entry time. Autonomy graded ai-led rather than autonomous: the published prompt supplies more than the problem. It instructs the model to assume for purposes of the task that a complete affirmative proof exists, enumerates the approach families to explore including the flow formulations the proof in fact used, and specifies the 64-agent search strategy in detail.

Virtual unwrapping itself is older (Seales read the En-Gedi scroll in 2015), but that worked because its ink contained metal and showed up in X-ray. Herculaneum ink is carbon-based and nearly invisible to tomography, which is why the ink signal had to be learned from texture instead of density. No Herculaneum scroll had been read by any method before this programme.

Readings are probabilistic reconstructions from a learned ink signal, not photographs of text: characters come with varying confidence and papyrologists supply conventional editorial restoration on top. The project's papyrology team reviews prize submissions, but that team is part of the challenge rather than an outside body, and no peer-reviewed critical edition of PHerc. 1667 had appeared when this entry was written, hence author-verified rather than independent. The attribution to Philodemus rests on a title read in a different scroll.

Machine-learning screening of superconductor candidates is an established and crowded field, and the JHU APL work on novel superconductors predates this. What is claimed as new is the end-to-end path: candidates identified from scratch by a machine-learning-guided pipeline, then synthesized and experimentally confirmed, rather than screening validated only against already-known superconductors. YRu3B2 and LuRu3B2 were not previously reported as superconductors. Whether this is the first such end-to-end confirmation is the consortium's framing and is not independently adjudicated here.

The gap between prediction and measurement is the story the coverage mostly buries: the screen selected for DFT-predicted Tc above 5 K, and the two compounds actually measured at 0.81 K and 0.95 K, roughly a factor of five to six low. These are sub-1-kelvin superconductors, nowhere near room temperature, and the consortium's stated goal of a room-temperature superconductor by 2033 is a research programme, not a result. Two confirmed compounds out of 741 stable candidates is also not a hit rate the paper establishes as generalizable. The specific machine-learning method is not named in the coverage consulted, so model is recorded as Unknown.

The numerical observation that a + b = 1 in the FullRSB jamming solution dates to the 2014 work of Charbonneau, Kurchan, Parisi, Urbani and Zamponi on the exact mean-field theory of hard-sphere glasses, where the relation was reported as observed but unexplained. It remained without analytic derivation in the subsequent literature. The derivation is new.

Peer-reviewed and published, which is the appropriate grade for a physics result of this kind, but this is an analytic derivation within an established mean-field framework rather than an independently replicated calculation. Autonomy graded collaborative: the model supplied the key idea, but its first formal write-up contained errors that the human authors fixed and verified, and the authors framed the exchange as asking for help on a problem they posed.

The Erdős problems were listed as open in the erdosproblems.com database and the OEIS conjectures as unproven at the time of the run; the paper documents which. In the course of the work the authors found misformalizations in the stated problems #125 and #741(i), which had to be corrected before resolution, a reminder that 'open' status in a database is itself fallible. Terence Tao's community wiki independently tracks AI contributions to Erdős problems and records these.

The headline is a hit rate, not a sweep: 9 of 353 and 44 of 492. The authors state successes concentrate in combinatorics, convex optimization and number theory where Lean's library is mature, that the agent inherits its LLM's biases and shows high search variance, and that it cannot solve problems requiring substantial new theory. Formal verification guarantees the proofs are correct; it says nothing about whether the problems were deep. Autonomy is graded search-scaffold rather than autonomous: humans built the agent, chose the problem sets, and supplied the formalization targets.

The unit-distance problem dates to Erdős (1946). Prior bounds were well documented; the construction is new.

Human mathematicians shaped the problem framing and verified the construction. The explicit n^1.014 exponent is Sawin's refinement, not the model's output: the model's own bound was inexplicit. The strength of the endorsement from Gowers is notable but is a judgment, not a formal check.

Computationally designed and consensus or mosaic antigens have a long history in HIV and influenza vaccine work, and broad sarbecovirus vaccine candidates were pursued by several groups after 2020. What is new here is a first-in-human safety and immunogenicity readout for an antigen with no natural sequence, generated computationally rather than selected from circulating strains. Searched PubMed for prior phase 1 results on pan-sarbecovirus immunogens; earlier candidates in this class were preclinical at the time of publication.

Phase 1: safety, tolerability and immunogenicity only. No efficacy claim, and immune response is not protection. n=39, healthy adults 18 to 50, so nothing follows about older or immunocompromised populations. Approval is years away and a phase 2 is planned. The autonomy grade is deliberately conservative because the public record is thin on what the computational method actually was: the reporting says artificial intelligence and machine learning without naming a model, architecture or developer, so model is recorded as Unknown rather than inferred. The bat-virus immunogenicity result is a laboratory assay against viruses that have not infected humans, not evidence of protection against a future outbreak.

The compound is new by construction: the generator is restricted to a combinatorial space of unsynthesized products, and the paper reports the 79 tested molecules as unique relative to the training set, with structural-novelty filters applied against known antibiotics leaving seven. The prior art in this registry is the 2020 halicin screen and the 2023 MRSA structural class, both of which selected from existing libraries; the distinguishing claim here is generation of a molecule nobody had made, followed by synthesis and an in vivo test. Searched PubMed and Europe PMC for synthecin: the only records are this paper and its 2025 bioRxiv preprint. The framework itself is an increment on the authors' own SyntheMol, which they state.

Preclinical. One compound, one pathogen, one mouse wound model, and topical administration; the paper describes systemic use as a possibility to be optimized toward, not a result. Structural novelty is measured by the authors' own filters rather than by an outside assessment. The 13 active compounds out of 79 synthesized is a hit rate on a set the model itself chose, so it is not an unbiased estimate of the generator's precision. Autonomy graded search-scaffold rather than ai-led: humans set the objectives, the scoring functions and the building-block space, and selected which candidates to synthesize, which is the same shape as the halicin and MRSA entries.

Documented as a new observation in the Quanta coverage; the specific structure was not previously catalogued.

The paper is an arXiv preprint, not yet peer reviewed, so this entry was downgraded from 'peer reviewed' once the artifact was located. The five authors are academic mathematicians unaffiliated with the announcing lab, and they turned AlphaEvolve's suggested permutations into proved theorems, which is what the 'independently checked' grade rests on.

Recorded as open in the Erdős problems database prior to resolution. Terence Tao's AI-contributions wiki tracked the resolution and did not find the result in existing literature.

Tao cautioned that the win 'says more about speed than difficulty': the problem was open but not considered deep. Lean formalization makes correctness essentially certain; significance is the contested part, not validity.

Not applicable. This is a meta-report, not a single claim.

Lab-authored evaluation of its own model. Individual case studies vary widely in strength and several have not been independently checked.

Prior bounds are cited per problem in the 81-page paper, with data and prompts released publicly. Tao flags the central novelty risk himself: for well-known problems the tool often proposed the optimal construction immediately, suggesting recall from training data rather than search, and one supposedly new four-dimensional Kakeya construction turned out to essentially match a prior Bukh–Chao paper. Entries in this registry drawn from the earlier AlphaEvolve release (kissing number, minimum overlap, matrix multiplication) are tracked separately.

Tao's own framing is that the contribution is scale and adaptability, not a fundamental breakthrough, and he describes the LLM as supplying 'educated randomness' inside an evolutionary loop rather than doing symbolic reasoning. Substantial human expertise was required to design non-exploitable verifiers: the system reliably finds loopholes, such as placing points at nearly identical locations to satisfy a distance tolerance. Included here because the negative and null results are reported alongside the wins, which is rare and is what makes it citable.

By definition, that is the whole point of the episode. The solutions existed in the published literature; GPT-5's contribution was locating them, a genuinely useful literature-search result that was misdescribed as original problem-solving.

Retained as a cautionary entry and a direct companion to the GPT-5 convex-optimization case. The underlying literature search was real and valuable; only the 'solved previously unsolved problems' framing was false. This is distinct from the later, genuine GPT-5.2 + Aristotle resolution of Erdős #728.

The theorem extends Aaronson's 2008 QMA oracle separation and a 2025 result of Jeffery and Witteveen; no prior bound of this form on black-box amplification appears in the literature. The AI contribution is documented in the paper's acknowledgements and on Aaronson's own blog, not inferred from press coverage. That matters, because most "AI proved a theorem" stories are not.

An arXiv preprint. The contribution is one lemma inside a human-conceived and human-written paper; Aaronson is explicit that the model did not pose the problem or design the argument and that he could have done the step himself given time. Autonomy is ai-assisted, which stays the right grade even though the step was pivotal.

Stable self-similar blow-up for these equations was already known, including Chen and Hou's computer-assisted proof for 3D Euler with boundary. Unstable singularities had been found only in isolated cases because they are numerically repelling; no systematic families existed in the literature. This is the first paper to produce several unstable families across three different equations by one method.

An arXiv preprint, not peer reviewed at the time of this entry. These are high-precision numerical solutions, not theorems: converting them into proofs requires a computer-assisted verification step the paper leaves to future work. No singularity for 3D Navier–Stokes, the Millennium Prize problem, is claimed, and the equations studied are not that one. Autonomy is search-scaffold: the equations, the self-similar ansatz and the loss function are human-designed and the network is the solver.

Synthetic phage genomes assembled from natural sequence date to Venter's 2003 ΦX174 reconstruction, and generative design of individual proteins was well established. Generating an entire genome that yields a working organism had not been demonstrated. The claim is bounded to bacteriophages, which infect bacteria only.

Peer review does not replicate: no independent group has rebuilt these genomes, and the 16 viable designs remain the authors' own result. The designs are variants within one small, exceptionally well-characterised template (ΦX174, 5,386 bp), not free-form genomes, and 269 of the 285 that were built did not work. On biosafety, the authors excluded eukaryotic and human-infecting viruses from training and confine the work to phages; the result has nonetheless become a reference point in biosecurity debate, which is context this entry records rather than adjudicates. Science published a biosecurity perspective alongside the paper arguing for legally required screening of synthetic DNA orders. Note that some press coverage of the Science paper misattributes the work to OpenAI; the collaboration is Arc Institute and Stanford.

The prime number theorem is not new mathematics; the contribution is formalization. What was open was whether this particular formalization could be completed, and the surrounding claim is about speed. Recorded because formalization at this scale is a distinct kind of contribution and because the AI finished work humans had started and stalled on, rather than producing a new theorem. Prior art is the PrimeNumberTheoremAnd project itself, which this build reuses and which the README credits.

This is a formalization result, not a mathematical discovery: no new theorem was proved. The comparison to '18+ months' is not like-for-like: Tao and Kontorovich worked intermittently, and the repository explicitly reuses definitions and some proofs from their earlier PrimeNumberTheoremAnd project. Math, Inc.'s announcement states the agent 'relies on natural language scaffolding supplied by human mathematicians, and requires high-level expert guidance'; the proportion of human effort is not quantified, and neither Tao nor Kontorovich is quoted in it. Graded author-verified rather than formal: the artifact is public and Lean-checkable, but the README does not itself assert a sorry-free build and no independent audit of that is on the public record. Vendor-announced, so the framing carries the usual caution.

Version 2 of the source paper, published 2 April 2025, had already established the optimal 1.75/L bound, strictly stronger than the model's 1.5/L. The model was working from an earlier version and its result was superseded before it was produced.

The proof itself is valid; the novelty claim is not. Analysts noted the argument largely recombined known techniques in different notation. Retained as a cautionary entry: this is the single most common failure mode in this space, and the reason every entry carries a novelty check.

Formal IMO results are not new (AlphaProof solved three 2024 problems in Lean), but a gold-medal-level score with a formal proof for every claimed solution had not been reported. The problems have published official solutions, so this is a capability milestone rather than new mathematics.

Problems had to be stated formally in Lean before the system could attempt them, the same human step that capped AlphaProof's autonomy grade. Answer-construction problems require the answer to appear in the formal statement, a known weakness of formal olympiad evaluation. No IMO-certified grading and no independently enforced contest time limit. The `formal` grade covers the proofs Aristotle produced, not the claim that this equals a human gold medal.

IMO problems have published official solutions, so this is a capability milestone rather than a new mathematical result, and the registry records it as one. The prior best was AlphaProof and AlphaGeometry 2's 28/42 in 2024, which required humans to hand-translate each problem into Lean first; removing that step is the substantive change.

Benchmark performance on problems with known answers, not a discovery. Google's own account describes training on a curated corpus of high-quality solutions and providing general guidance on how to approach IMO problems, which is human mathematical input beyond posing the problem, hence ai-led rather than autonomous. Problem six went unsolved. The parallel OpenAI claim is self-graded and not IMO-certified, and drew criticism for being published before the closing ceremony, which organisers had asked AI developers to wait for.

AI-generated molecules had reached the clinic before, and AI-nominated targets had been published before, but this is the first randomised placebo-controlled efficacy signal for a compound where both the target and the molecule came from generative systems. TNIK's role in fibrosis was not an established target hypothesis when it was nominated.

Phase 2a is small, short and exploratory: 71 patients over 12 weeks, single-country sites, not powered for efficacy, with FVC change over 12 weeks not a registrational endpoint. The sponsor designed, ran, analysed and published the trial. "AI-discovered" covers target selection and generative chemistry; the medicinal chemistry, preclinical work and trial conduct were conventional. A Phase 3 was subsequently initiated, which does not retrospectively strengthen this readout.

Strassen (1969) and subsequent literature exhaustively catalogued; 49 was the standing record for complex-valued 4×4. Confirmed new.

Applies to complex-valued matrices specifically. Practical speedup is limited; the significance is theoretical. Related follow-up work by others has explored rank-23 schemes for 3×3.

Kissing number bounds are well catalogued per dimension; the 11D improvement was checked against the standing record.

A lower-bound improvement via explicit construction, not a resolution of the problem. The 20% improvement rate means most of the 50+ problems saw no advance.

The minimum-overlap constant and the autocorrelation inequalities have well-tracked records. AlphaEvolve's values were compared against the standing bounds and confirmed to improve them.

The improvements are marginal in magnitude, and both were improved again by other automated systems in 2026. As with the other AlphaEvolve results, a human-designed evaluator and search loop did the selecting.

Ripasudil is a clinically used Rho kinase inhibitor; the paper states that to the authors' knowledge it had never previously been proposed for the treatment of dry age-related macular degeneration, and the peer-reviewed version carries that claim. The ABCA1 mechanism emerged from the system's own follow-up experiment rather than from the prior literature. What is new is the repurposing hypothesis and its in vitro support, not a new compound.

Peer reviewed, which is the right grade for an empirical claim of this kind, but in vitro efficacy is a long way from a treatment: a candidate is many years and several trial phases from the clinic. Verification of the biology is the journal's, not an independent replication. Autonomy stays ai-led rather than autonomous: the paper describes the approach as semi-autonomous, and humans executed every physical experiment, though all hypotheses, experimental directions, data analyses and main-text figures were produced by Robin.

Machine-written text had passed review before in the form of nonsense-generator stings (SCIgen, 2005), which tested review rather than produced research. The claim here is different: an autonomous pipeline produced a real experimental paper that reviewers rated acceptable. Sakana's own write-up is the source for the process, and the code and submitted manuscripts are public.

Workshop tracks accept a far higher share of submissions than the main conference, and Sakana says so itself; the company also notes the accepted paper contains a citation error and that its own reviewers judged the work below the main-conference bar. The paper's scientific content is a negative result: the proposed regularisation did not help. Reviewers were not told which submissions were machine-generated, but the experiment ran with organiser consent, so this is not a blind test of peer review at scale. Humans chose the venue and selected which generated papers to submit, which caps autonomy at ai-led.

The AMR mechanism proposed had reportedly been independently arrived at by a human group whose work was unpublished at the time, which complicates the novelty claim.

Hypothesis generation with human-run validation, not autonomous discovery. Peer review confirms the work, not that every hypothesis in it was unprecedented, and the novelty question above is untouched by publication. Independent replication outside the collaborating labs is limited. Graded conservatively.

De novo enzyme design dates to the 2000s (Kemp eliminases, retro-aldolases), but designed enzymes were typically orders of magnitude slower than natural ones and needed directed evolution to become useful. The advance is reaching this efficiency with multi-step catalytic machinery by design rather than by evolution.

Serine hydrolases are a comparatively tractable target with a well-understood catalytic triad; the result does not generalise automatically to harder chemistry. Efficiencies remain below the best natural hydrolases. The per-round success rate is low and the paper reports the screening funnel. The reaction, the active-site description and the assays were human-specified, which is why autonomy is search-scaffold.

Engineered GFP variants are routine but sit a handful of mutations from a natural template, and directed evolution moves in small steps. A functional fluorescent protein this far from any known sequence had not been reported, and the paper includes the expression, spectra and brightness measurements rather than a prediction alone.

The 500-million-year figure is an inference from a sequence-divergence-to-time calibration, not a measurement, and has been criticised as a marketing frame. esmGFP was one hit from a generated and screened set; the paper reports the funnel. The design goal and the chromophore constraint were supplied by humans. No independent re-synthesis of esmGFP by an unaffiliated lab was on record when this entry was written.

Generative models for crystals existed (CDVAE, and screening pipelines like GNoME); the contribution claimed is property-conditioned generation validated experimentally. The novelty question is precisely what is disputed below: whether the synthesised compound was new.

A published critique in Materials Horizons argues the synthesised disordered phase Ta₁⁄₃Cr₂⁄₃O₂ is the same material as Ta₁⁄₂Cr₁⁄₂O₂ reported in 1972, that this compound is present in MatterGen's training set, and that its composition differs from the reported TaCr₂O₆, i.e. the flagship validation recovered a known material rather than a new one. The generative method itself is not refuted; the disputed part is the experimental novelty claim, and the entry is graded on the strength of that published objection. This registry keeps entries like this one rather than removing them.

Machine-learning decoders had been proposed for years but had not beaten the best classical decoders on real hardware data at scale. The result is a decoder that does, on a specific processor.

Accuracy, not speed: AlphaQubit is far slower than matching decoders and does not run inside the real-time budget a fault-tolerant machine needs, which the paper states. It is trained per device on that device's data, so it does not transfer for free. Scaling behaviour beyond the tested code distances is open. This improves a component of error correction; it does not itself demonstrate a fault-tolerant computation.

Complete connectomes existed for C. elegans (302 neurons, 1986) and the Drosophila larva (3,016 neurons, 2023). This one is roughly 45 times larger than the previous largest complete connectome, and automated segmentation is what made that scale reachable at all.

Automated segmentation alone was not accurate enough: the result required years of human proofreading, which is why autonomy is graded ai-assisted rather than ai-led. Neurotransmitter identity is predicted rather than measured for most connections, and gap junctions and neuromodulation are not fully captured. It is one individual's brain, and a wiring diagram is not by itself an explanation of behaviour.

These are competition problems with published official solutions, so the achievement is a capability milestone (solving hard, known-answer problems under near-competition conditions) rather than a new mathematical result. The registry records it as such.

Problems were hand-translated into formal Lean statements by people before AlphaProof attempted them, a real human contribution beyond posing the question, so autonomy is graded conservatively. AlphaProof also took far longer than the human time limit on some problems. This is benchmark performance on solved problems, not a discovery.

Nothing loads from YouTube until you press play.

Docking and complex prediction had decades of specialised tools (AutoDock, RoseTTAFold All-Atom, and AlphaFold-Multimer for protein assemblies). The contribution is one model spanning molecule types at higher accuracy, not a new biological result; the structures it predicts are natural ones.

At publication neither code nor weights were released, only a rate-limited web server, which drew an open letter from over a thousand researchers about reproducibility; weights for academic use followed in November 2024. Accuracy on antibody–antigen complexes and some nucleic-acid targets is far below the headline figures, and the model can produce confidently wrong hallucinated structure in disordered regions. Predictions are hypotheses, not measurements.

Distinct from the 2022 DeepMind–TCV work already in this registry, which learned magnetic shape control rather than instability avoidance. Tearing-mode prediction from machine learning had been published before; closing the loop so the controller acts on the prediction during a live shot is the new part.

Demonstrated on one machine in specific scenarios. A data-driven controller trained on DIII-D discharges has no guarantee of transferring to another tokamak, still less to ITER-scale burning plasma where the training data does not exist. Tearing modes are one disruption pathway among several. The physics model, actuators and safety limits are human-designed; the policy operates inside them.

Automated geometry provers date to Wu's method in the 1970s and to GEX/Java Geometry Expert; the prior state of the art solved 10 of the 30 benchmark problems. The benchmark is IMO geometry problems from 2000–2022 with known solutions, so the contribution is the method and the score, not a new theorem.

Benchmark performance on solved problems, not a discovery. The domain is narrow: plane geometry expressible in the system's formal language, which excludes problems involving inequalities or variable numbers of points, and the benchmark set was filtered to what the language can state. Proof steps are machine-checked by the deduction engine, which is what carries the confidence; the peer-reviewed grade reflects Nature review of the system and results.

Robotic synthesis platforms and automated reaction optimisation predate this (Cronin's mobile robotic chemist, Nature 2020, among others). What was new is a general-purpose language model doing the planning, tool selection and code generation across unfamiliar hardware from a natural-language goal, rather than executing a human-written protocol.

The chemistry performed is textbook cross-coupling: the finding is about autonomy, not about a new compound or reaction. The paper's own safety section shows the agent could be steered toward hazardous syntheses and the authors call for safeguards. Humans set up the hardware, reagents and safety envelope, and the tasks were chosen to be within the platform's reach.

This is the same group's follow-up to the 2020 halicin work and to abaucin (2023); the new element is selecting a structural class via model interpretation instead of screening for individual hits. "New structural class" is a claim about scaffold novelty relative to clinical antibiotics, checked against known antibiotic chemotypes in the paper.

These are candidates, not drugs: mouse models only, with no clinical development at the time of this entry. The mechanism, disrupting membrane potential, is the same one halicin uses, so the novelty is structural rather than mechanistic, and membrane-active compounds carry a known mammalian-toxicity risk. The screening library, assays and interpretation were human-run; the model scored and explained.

Cap set bounds are a well-tracked literature; the constructions were confirmed to exceed the standing record at publication.

The LLM proposes; a human-designed evaluator and search loop does the selecting. Calling this 'the AI discovered it' overstates the model's role, though the discovery is real.

Compared against best-fit and first-fit families and published heuristics; improvements are empirical on tested distributions.

An empirical improvement on benchmark distributions, not a proved worst-case bound.

Stable-material prediction builds on the Materials Project and OQMD convex-hull databases. The dispute below is precisely about how much of GNoME's set is genuinely new relative to those existing catalogues.

Substantive objections were raised and remain unresolved. Cheetham and Seshadri, reviewing the release, found 'scant evidence for compounds that fulfil the trifecta of novelty, credibility and utility,' noting that many entries are minor substitutional variants, radioactive, or otherwise unlikely to be useful. Stability here means a DFT convex-hull prediction, not experimental synthesis; the headline counts are predicted, not made.

Targets were drawn from computed stability databases. The contested question is whether the synthesised phases were correctly identified and genuinely new, rather than known phases or misindexed results.

A detailed critique led by Robert Palgrave argued that many of the 41 claimed compounds were misidentified from the X-ray data, in several cases likely known phases, mixtures, or amorphous products rather than the claimed novel crystals. It is the identification step, not the automation, that is disputed; the autonomy claim itself is not the weak point. A 2026 Author Correction from the team re-analysed the diffraction data and clarified that 'novel' was meant as new to their prediction platform rather than necessarily new to science.

Machine-learning weather models existed before (FourCastNet, Pangu-Weather), and Pangu had already reported beating HRES on some measures. GraphCast's contribution is the breadth of the win across variables and lead times, at operational resolution, with public code. That is what moved national weather services to adopt learned models.

GraphCast is trained on ECMWF reanalysis and initialised from ECMWF analyses, so it depends on the physics-based system it is measured against rather than replacing it. Deterministic models trained on a mean-squared-error objective blur fine structure and underestimate extremes such as peak cyclone intensity. It has no conservation guarantees and cannot forecast anything outside its trained variables. Later ensemble models such as GenCast address part of this.

Variant-effect predictors are a crowded field (SIFT, PolyPhen-2, EVE, CADD). The contribution is proteome-wide coverage at state-of-the-art benchmark accuracy without training on clinical annotations, which is what makes the predictions usable where no clinical data exists.

These are predictions, not diagnoses, and DeepMind says so: ACMG/AMP guidance treats computational evidence as supporting rather than standalone. Benchmarks have been criticised for circularity, since the model trains on population frequency and is evaluated partly against datasets encoding related signals. Calibration varies by gene, and a "likely pathogenic" call on a variant nobody has seen in a patient remains a hypothesis.

The libc++ small-sort routines had been hand-optimised by compiler engineers for years. AlphaDev's shorter instruction sequences were reviewed against the standing implementations and confirmed to be improvements before being merged.

The gains are on very short fixed-length inputs; asymptotic sorting complexity is unchanged, and the headline percentage speedups apply only to those small cases. The 'independent' grade rests on LLVM maintainers reviewing and merging the code, not on a formal proof of optimality.

Nothing loads from YouTube until you press play.