Axiom released a public Lean development that it describes as the first complete computer-checked proof of the classification of finite simple groups. The project reports 43.1 million lines, 2.05 million declarations and a dependency map drawing on 715 papers and books; Axiom says dozens of AI agents, directed by mathematicians and engineers, produced it over 24 days. The associated investigation reports 34 noteworthy deviations from the published literature. Its largest intervention concerns a closure assertion in one route to the Unbalanced Group Theorem: a companion paper by Colin Defant and Ken Ono gives a counterexample to that assertion and an alternative simple-group argument based on Solomon’s maximal 2-components, including a new “preservation of simple tops” theorem. The repository exposes the Lean project, comparator configuration and certificates, while the interactive site provides a proof map.

Anthropic deposited “A 2^{o(n)} Time Algorithm for 3-SAT,” claiming a deterministic subexponential algorithm for 3-SAT and the harder exact-counting problem #3-SAT. According to the paper’s provenance account, an internal Claude research model found the core algorithm on October 16 using about 14 million output tokens without human input; Anthropic researchers then worked with Claude on presentation. The public formal-math repository now contains an eth project and describes a checking workflow using a pinned Lean toolchain, comparator statements and the independent nanoda kernel. This is a genuine update to the previous digest’s OpenAI ETH item: Anthropic claims a concurrent, independent discovery of a similar result rather than merely commenting on or formalizing OpenAI’s manuscript. Ryan O’Donnell also published an LLM-assisted exposition on October 27 highlighting the parity-approximating polynomial and its matrix formulation.

In a supplied direct X thread, Thomas Bloom cautioned that the recently announced OpenAI local-smoothing proof does not make the Wang–Zahl approach redundant. He pointed to the earlier Lai–Pang–Sethi–Wang preprint, submitted on October 7, which studies the (n−2)-plane Kakeya problem in R^n for n at least four under convex Wolff axioms. Bloom’s distinction is that OpenAI’s route reportedly yields consequences beyond ordinary Kakeya, including Fourier restriction, while the Wang–Zahl technology extends in a different direction to generalized (k,n)-dimensional Kakeya questions. He explicitly said that the full scope of both approaches remains unclear.