mt0-svg: AI-made Tammes N=15, Robbins V>2, frog model (Lean)

On Oct 18 the sweep’s Zenodo check turned up “The Tammes problem for fifteen points” (v1.4.0). Its author is listed only as mt0-svg, and it opens with: “This is AI-generated research: the results, proofs and code were found and written by AI.” The same GitHub account had released five more such papers since Sept 28. Each comes with a Lean 4 development, a comparator challenge, CI that rebuilds everything, and computation certificates.

• Tammes, N = 15. The paper extends the Musin–Tarasov method used for 13 and 14 points: a written reduction to irreducible contact graphs, an interval-arithmetic search with recorded and replayed trees, and a local rigidity estimate near the two known optima. Lean proves everything except that the plantri enumeration is complete and that the Rust program matches its formal model; those enter as stated hypotheses. Exactly two non-isomorphic optimal configurations exist. That answers Musin and Tarasov’s question whether the maximal contact graph is unique (it is not, for N = 15). The two-configuration classification (Theorem 1.3) was contributed by GitHub user Satvik-patil in an issue that says it was “produced with an AI system (Claude)”.
• Robbins’ problem. It asks for the least expected rank of a value chosen by a stopping rule from n i.i.d. uniform values with full information. The paper relaxes it to a memory of the five smallest values seen and certifies V(n) > 2.0038 for n ≥ 300. That answers Bruss and Ferguson’s 1996 question whether V > 2. The Lean proof has no hypotheses beyond the definitions.
• Frog model. Recurrence on the rooted 3-ary tree and transience on the 4-ary tree, the cases Hoffman, Johnson and Junge left as a conjecture, proved through exact recursions on subtree response laws, with certificate checkers verified in Lean.
• Smaller items: a counterexample to Keith–Zanello’s Conjecture B at p = 73, a proof of Furio–Lombardo’s conjecture that a twist of the Klein quartic has exactly four rational points, and κ = 3 for doubly uniform regret in 1D online linear regression.

Web searches on Oct 18 found no news coverage, no posts by experts and no Hacker News thread. The repos had no stars.

If they hold up, these are real advances on named problems. The Tammes problem is a classical problem in discrete geometry, and each new case so far has needed a major computer-assisted effort. Robbins’ problem is one of the best-known open questions in optimal stopping. The account names no model and no person, so we cannot tell which system made them or how much human direction there was. The Lean proofs and certificates are public and can be checked, which is not true of many AI maths claims. The Tammes proof’s trust boundary (enumeration and program correctness) is stated explicitly.