Logic, foundations, computability and proof systems.
If a graph is not countably colorable, h_G(n)/n tends to infinity, where h_G(n) is the largest minimum number of edge deletions needed to make an n-vertex subgraph bipartite. Equivalently, a uniform linear deletion bound on all finite subgraphs forces countable colorability. The limit holds for the whole sequence, for graphs of any uncountable chromatic cardinality.
A Gemini agent pipeline discovered and formally proved closed systems of Collatz-like acceleration rules for eleven specified six-state, two-symbol Turing machines. Each system summarizes exact execution from its fixed blank-tape starting configuration; the machines’ eventual halting behavior remains unresolved.
For any pure type system, if every legal expression in every valid context has a terminating β-reduction sequence, then every β-reduction sequence from every such expression terminates, including reductions inside type annotations.
A finitely generated group has decidable word problem if and only if it embeds in a finitely presented simple group.
Every recursively enumerable subset of natural-number n-tuples, for n≥1, has an integer-polynomial Diophantine representation with exactly one complete natural-number auxiliary tuple for each member and none for nonmembers.
OpenAI reports that no algorithm can decide whether an integer-coefficient polynomial has a rational solution when the number of variables is part of the input.
OpenAI reports that every order automorphism of the full Turing-degree partial order is the identity in ZFC, without a definability or regularity restriction on the automorphism.
OpenAI reports that consistency of ZF implies consistency of ZF plus the Partition Principle and Choice for ordinal-indexed families but without the full Axiom of Choice.
OpenAI claims that every infinite Löwenheim–Skolem bound admits a uniform threshold above which one categorical cardinal forces categoricity throughout the remaining tail, in ZFC.
Every finitely generated group with decidable word problem embeds injectively in a nontrivial simple group of type F∞, meaning it has a classifying CW complex with finitely many cells in each dimension.
OpenAI claims a group of type F∞ containing every finitely presented group. Its finitely generated subgroups, up to isomorphism, are exactly the finitely generated recursively presented groups.
Kegel, Li and Ren give an effective family of finite presentations with two generators and ten relators for which deciding triviality is impossible. The count is an achieved presentation size, not a minimum.
Kegel, Li and Ren give an effective family of finite presentations with four generators and eleven relators for which deciding triviality is impossible. These are fixed presentation slots, not a minimality result.
Kegel, Li and Ren give a finite presentation with three generators and nine relators whose word problem is unsolvable. The count is an achieved presentation size, not a minimum.
The model-extracted generic polynomial-calculus/Res(parity) sufficient criterion in Theorem 9.1, rather than attributing the complete bit-PHP lower-bound architecture to AI.
Almeida and Knudstorp report that Medvedev’s logic of finite problems is undecidable, by reducing periodic plane tiling to non-theoremhood.
Chernikov constructs a complete simple theory with a definable group and a global type whose left-translation orbit has size at most 2^ℵ₀, although the group has no left-invariant Keisler measure. This refutes the bounded-orbit implication to definable amenability outside NIP.
There is a divergent integer-valued function f such that if every finite n-vertex subgraph of a graph becomes bipartite after at most f(n) edge deletions, then the graph has finite chromatic number. The formal proof gives three-colourability.
For cut-defined omnific integers a,b,c,d represented as numeric games, a Lean theorem says ab=cd implies omnific e,f,g,h with a=ef, b=gh, c=eg and d=fh, including zero cases. The theorem is stated at each Lean universe, rather than putting all surreal numbers into one type.
Freitag and Mutchnik give a stable theory of an infinite-dimensional vector space over the division ring of fractions of the quantum graph algebra of the random graph, refuting stable forking.
The free Heyting algebra F₂ on two generators cannot be the lattice of subterminal objects of an elementary topos. The obstruction extends to any Heyting algebra surjecting onto F₂, including free F_N for N≥2.
For Borel-definable global Keisler measures over a model of a discrete first-order theory, the authors prove the reverse implications: self-averaging gives a definable measure whose canonical random extension is generically stable, which in turn gives a frequency interpretation measure. Together with earlier forward implications, these yield equivalence.
A ZFC model has the property that every family (Aₓ) of subsets of ℝ with outer measure below one admits an infinite X such that x∉Aᵧ for distinct x,y∈X. Combined with Hechler’s earlier CH counterexample, this gives relative ZFC independence for the first question of Erdős 501.
For every complete first-order theory, SOP₂ implies SOP₃. The reverse implication was already known, so the two dividing lines coincide.
For every subDL theorem A → B, GPT-5.6 Sol’s terminal-hierarchy argument claims that A and B share a variable with the same sign at the same relevant-arrow depth.
For k≥1 and δ,ε>0, Theorem 1.14 extracts an ε-tight uniform (k,δ)-ladder from a (t,2δ+ε)-tree at some depth t≤(1/ε)^(O(k/ε²)), avoiding a multicolored Ramsey step.
Some computably enumerable truth-table degree contains no computably enumerable irreducible many-one degree. Cintioli derives the example using Degtev’s c.e. semirecursive set with rigid complement and the fact that its simple-set representatives cannot be irreducible cylinders.
An infinite-chromatic graph has the property that, for every nonnegative function f(m) tending to infinity, every m-vertex finite subgraph contains an independent set of size at least m/2−f(m). A stronger construction bounds local odd-cycle-transversal number by any prescribed unbounded integer profile.
For semifree noncommutative differential graded algebras over a nontrivial computable unital commutative ring, stable tame isomorphism, quasi-isomorphism and derived Morita equivalence are undecidable.
Logic, foundations, computability and proof systems. Individual results follow their mathematical subject, regardless of how their proofs were checked.
Publication dates and editorial changes.
At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier
Erdős Problem 111: bipartizing finite subgraphs of uncountably chromatic graphs
OpenAI reports simple F∞ overgroups for decidable-word-problem groups
AI-assisted positive model makes Erdős 501 independent of ZFC
ChatGPT-assisted construction refutes Petrykowski’s conjecture
GPT-6 Astra resolves Erdős Problem 74 on local bipartiteness
AI-built Lean proof reports Conway’s omnific refinement property
ChatGPT-assisted argument sharpens tight-threshold extraction
Gemini-discovered example answers Odifreddi’s degree question
AI-developed two-generator family has undecidable triviality
AI-developed four-generator family has undecidable triviality
AI-developed construction gives a nine-relator group with unsolvable word problem
OpenAI reports weak-to-strong normalization for pure type systems
AI-assisted classification of depth-labeled substitutions in Sacchetti logics
Allow optional Google Analytics to help improve AIProofWatch? Privacy details.
