OpenAI released a manuscript and Lean artifact claiming that, for every fixed k, satisfying assignments of a k-CNF with n variables and m clauses can be counted deterministically in polynomial space and time (n+m)^{O_k(1)}·2^{O_k(n log log n/√log n)}. For bounded clause density the manuscript states the sharper exponent O(n/√log n). Either bound is subexponential in n and would refute the Exponential Time Hypothesis for 3-SAT. The public Lean scope document states a slightly weaker general encoded-input bound, with an extra log log n factor, but that bound would still be subexponential. OpenAI says the natural-language result was found on October 16 and formalized on October 17; the manuscript was revised October 25 and publicly announced October 26.

OpenAI released natural-language and Lean artifacts claiming the Euclidean half-wave local-smoothing estimate in every dimension n≥2 throughout the expected range, with arbitrarily small positive Sobolev loss, including the critical three-dimensional L³ estimate. The formalization’s scope also states Bochner–Riesz, spherical-extension and Stein square-function estimates in strict ranges, an Lⁿ Kakeya maximal estimate with δ^{-ε} loss, and full Hausdorff dimension for Euclidean Kakeya sets. OpenAI says its model produced the argument on October 18 and it was formalized the next day.

Scott Armstrong released a Lean 4 and Mathlib development corresponding to the eleven-author paper “The Critical 2D KPZ Process,” previously reported in this digest on October 22. The repository says it formalizes the paper’s convergence and structural results for the critical stochastic heat flow and KPZ process, plus four additional results. It provides Mathlib-only restatements, comparator checks for definitions and theorem statements, and replay through Lean and the independent NanoDa kernel. The repository explicitly records that the paper’s authors have not reviewed the formalization and that some statement deviations are documented.

A new public Lean 4 development formalizes regularity structures and the construction of the dynamical Φ⁴₃ model on the three-dimensional torus, following Hairer’s 2014 work. The repository states the renormalized equation and convergence result, contains no sorry in the library, lists 23 main results, and supplies six comparator configurations for major theorem statements. Its verification workflow includes pinned Lean and Mathlib versions, axiom checks, automated searches for sorry, and replay of selected solutions through both Lean and NanoDa. Armstrong says AI coding agents wrote the proofs under his supervision, with exact definitions and statements approved before proof development and separately compared with sources.

AGMAI clarified its proposed workflow for releasing AI-generated mathematics. It recommends against AI companies selecting particular mathematicians to receive or lead interpretation of results, arguing that advance or privileged access can distort credit, participation and community agency. On October 26 it applied that principle to OpenAI’s announced Yang–Mills, QCD and Standard Model work, asking for immediate release of the natural-language and Lean artifacts rather than waiting for a designated group’s exposition. Timothy Gowers and Thomas Bloom amplified the clarification; Bloom disclosed that he and Gowers had previously received OpenAI’s unit-distance counterexample before public release and said he did not think that arrangement should recur.