cert-machine · audit · a peer-reviewed release, replayed and read

AlphaProof Nexus: the proofs hold under two kernels; three OEIS conjectures were already proved, and two statements are degenerate

Google DeepMind’s AlphaProof Nexus (Science, October 2026; arXiv 2605.22763) reports that its agent “resolved 9 of 353 open Erdős problems” and “proved 44/492 OEIS conjectures”, the latter “correctly formalized and previously unproven”. Its results repository publishes the Lean proofs. Here every published Erdős proof — and the corrected #741(i) the paper says it also found — is replayed by Comparator against formal-conjectures’ own statement with two independently written kernels, and every published OEIS statement is read against the conjecture it claims, its definition checked against the OEIS terms. The proofs hold. What the release says about them holds less well.

Pinned: google-deepmind/alphaproof-nexus-results @ 0647711a (Lean v4.27.0, Mathlib a3a10db), formal-conjectures @ 7862bf6a (the commit the repository builds against) and @ e30c4c3d (today), the arXiv preprint v1 and the seven erdosproblems.com pages by digest, the 38 OEIS records and b-files, the MathOverflow thread behind A382590 — corpus/alphaproof-nexus, with every file’s sha256. Nothing of the claimant was run on this machine; the kernel lane ran on GitHub’s hosted runners. Decided: statement equality and kernel acceptance. Read, by an AI agent and re-checked before stating: what each OEIS statement says against its conjecture. Not decided: whether formal-conjectures’ Erdős statements are the problems Erdős posed (beyond the #741 density point), and the six OEIS proofs the repository does not publish.

tl;dr

The finding. Gaps, first. (1) 38 of the 44 OEIS proofs the paper counts are published. (2) Three of those 38 conjectures already had a proof on record before the preprint (21 May 2026), against the paper’s “previously unproven”: A325046 (Sela Fried, approved on OEIS 17 Dec 2025), A382590 (Terence Tao’s accepted MathOverflow answer, 31 Mar 2025), A237271 (equivalent, per OEIS, to an A384149 conjecture Hoft proved on 11 Jan 2026). (3) Two OEIS statements hold for a reason unrelated to their conjecture: A382590 counts prime factors with multiplicity, so its “k-th prime factor” is eventually the constant 2; A237271 defines the sequence by an already-proved characterization, which leaves a two-line divisor fact. (4) “9 of 353 open Erdős problems” counts formal statements: nine statements over seven problem numbers — two parts each of #12 and #741, and three variants, one of them (#26) not posed by Erdős. The paper’s Table 1 marks this; the abstract does not. (5) The published #741(i) proof is of the natural-density reading, which formal-conjectures demoted to a variant in August; the corrected upper-density proof the paper also counts is not in the results repository (it sits on formal-conjectures’ merged pull request #3778). It holds too.
The mechanism. What holds. All 10 kernel items are CERTIFIED: for each, Comparator builds OUR challenge — formal-conjectures’ statement file at the commit the repository builds against, the theorem renamed — and THEIR solution, byte for byte, in a sandbox, checks that the solution proves exactly the challenge’s elaborated statement with only propext, Quot.sound and Classical.choice, and replays it through Lean’s kernel and through nanoda, an independently written kernel. 10 jobs, 78–196 s each after the Mathlib cache. Textually too: the nine statements equal formal-conjectures’ at the pin, their definitions verbatim, nothing shadowed, no kernel-bypassing construct. All 38 OEIS definitions, translated into exact Python, reproduce the OEIS terms. Of the 38 OEIS statements: 32 match, 3 are narrower, 1 stronger (harmlessly), 2 degenerate.
Check it. Red controls, which must be rejected, are: a weakened challenge statement and a solution whose proof is replaced by sorry (Comparator: REFUTED?, REFUTED?); in the textual lane, five planted changes (a weakened bound, a flipped answer, a changed definition, a shadowing declaration, an axiom), all caught. Re-derive: python3 tools/apn-statements.py --check, python3 tools/apn-oeis.py --check, gh workflow run apn-kernel.yml -f items="…" then node tools/record-apn-kernel.js <run>.

§1 · OEIS

The OEIS conjectures: three already proved, two degenerate

The paper: “We used Gemini to autoformalize 492 open questions from the OEIS … The agent found proofs for 44 conjectures that a manual review found to be correctly formalized and previously unproven.” The repository publishes 38. Each was read against its OEIS entry by an AI agent not told what to look for; each definition was translated into exact Python and run against the OEIS terms; every row below was re-checked against the sources before it is stated here. The readings are AI-made and unconfirmed by a specialist, and they say what a statement does not say — never that a proof is wrong.

A382590 — degenerate. The Lean kth_prime_factor counts prime factors WITH multiplicity (primeFactorsList). The conjecture, as its MathOverflow source states it with examples (question 490330, asked 2025-03-31: "n = 2, N = 2: (3, 5, 7)"), counts distinct primes. The 2-adic valuation of a(n), from the Lean file's own recurrence, is 0, 1, 0, 0, 3, 1, 2, 7, 6, 10, 21, 27, 44, 77, 116, 188, 311, 493, 798, 1299, 2090, 3382, 5481, 8855, 14328, 23193 for n = 0..25; it is at least 3 from n = 7 on, so with multiplicity the 2nd and 3rd prime factors are 2 from there on and the "eventually periodic" statement holds by eventual constancy, not by the 3, 5, 7 cycle the conjecture is about. Terence Tao's accepted MathOverflow answer (2025-03-31) proves the conjecture for distinct primes (A_n divides A_{n+3}, so the k-th smallest prime factor is bounded, plus periodicity mod p); OEIS: "Terence Tao sketched the proof (see the Mathoverflow link)."
A237271 — degenerate given its definition. The Lean a is not the sequence's definition (parts of the symmetric representation of sigma) but Conjecture 1's characterization, which OEIS records as proved (Hoft, Jan 21 2025). Given it, the theorem (a n = the number of 2-dense sublists) is a two-line divisor fact: for consecutive divisors d < d', d' > 2d forces d' odd, since an even d' would put the divisor d'/2 strictly between them. OEIS: Conjecture 2 "is essentially the same as the second conjecture in the Comments of A384149", which A384149 records as proved (Hoft, Jan 11 2026) — before the preprint.
A325046 — already proved. The statement matches the conjecture. OEIS: "The conjecture is true (see Fried link). - Sela Fried, Dec 17 2025", with Fried's proof PDF; the OEIS history shows the edit approved Wed Dec 17 17:20 EST 2025 (corpus/alphaproof-nexus/oeis-data/A325046-history-excerpt.txt) — five months before the preprint (2026-05-21).
A309132 — stronger. The conjecture asserts one inclusion (composite and a(n) squarefree => Carmichael); the theorem is an iff, (is_composite n ∧ Squarefree (a n)) ↔ is_carmichael_number n, adding Carmichael => composite and a(n) squarefree. The added direction is already in the entry: Sondow's Theorem 2 (Jul 19 2019) and his proof in A309235 that a(m) | m for Carmichael m (Carmichael numbers are squarefree). So the open content is the same; read as "are exactly the Carmichael numbers" it would be MATCHES.
A113254 — narrower. The conjecture quantifies over all m (the whole family); the theorem is the single case m = 8: ∀ n : ℕ, IsSquare (a (2 * n + 1)) with the m = 8 recurrence | n' + 4 => -4 * a (n' + 3) + 256 * a (n' + 1) + 4096 * a n'.
A271591 — narrower. is_maximal_run requires the run to end (a (n + L) ≠ v), so the theorem only constrains runs that terminate. It does not exclude an eventually constant tail (an infinite run of 0s or 1s), which the conjecture ("only 4 or 5" / "only 3 or 4") does exclude. The omitted case is elementary to rule out from the tribonacci growth ratio (about 1.839 < 2), but it is not stated.
A002897 — narrower. The theorem states only the second, "If true, then" part (the coefficient identity): (a n : ℤ) = MvPolynomial.coeff (xyz_pow_n n) (P_n n). It does not state the diagonal claim. OEIS treats the two as "both parts of Bala's conjecture" (Easwar), and the AI comment says "The latter identity was proved". By MacMahon's Master Theorem the coefficient identity is equivalent to the diagonal claim: setting x = 1 in the degree-4n homogeneous form gives exactly P_n. So the omitted part is classical, not open mathematics.

Every definition agrees with the OEIS terms on the range its translation checks (from 9 to 10,000 terms; the ranges are in certs/apn-oeis.json). The translations re-run with python3 -I corpus/alphaproof-nexus/oeis-reading/run_all.py (about two minutes).

§2 · Erdős

Nine statements, seven problems, two kernels

The paper: “Our most capable agent autonomously resolved 9 of 353 open Erdős problems”, and, in Table 1’s caption: “Open problems from the ErdosProblems repository autonomously resolved by our full-featured agent. The asterisk indicates a variant of the main problem with this number. Problem #26 (annotated with †) is a more general variant of a question posed by Erdős, but was not posed by Erdős himself.” The 353 are formal-conjectures’ statements “at the time of the run”, parts and variants included.

erdos_12.parts.i — part, answer True. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_12.parts.ii — part, answer False. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_125.variants.positive_lower_density — variant, answer False. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_138.variants.difference — variant, answer True. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_152 — main, answer True. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_26.variants.tenenbaum — variant, answer False. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_741.parts.i — part, answer False. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED. Changed at formal-conjectures’ head: the main statement is now the upper-density reading; this one survives as a variant.
erdos_741.parts.ii — part, answer True. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.
erdos_846 — main, answer False. Statement equal to formal-conjectures’ at the pin; kernel lane CERTIFIED.

#741(i). erdosproblems.com: “The interpretation of this question with upper density most likely captures the spirit of the question.” The paper says the interpretation “was amended to … ‘upper density’ … after our full-featured agent found proofs using density as ‘natural density.’ Following the correction of the ambiguity, the agent was still able to resolve the questions.” The results repository publishes the natural-density proof; the corrected one is linked from formal-conjectures at commit 9d492049, the head of its merged pull request #3778. Both are CERTIFIED here.

§3 · method

How the kernel lane runs, and what was changed to run it

Comparator is the Lean FRO’s judge: it builds the challenge and the solution in a landrun sandbox, exports both with lean4export, compares every constant the theorem’s statement mentions, checks the axioms, and replays the proof through Lean’s kernel and nanoda. The repository is on Lean v4.27.0, and two declared amendments were needed, each found by a pilot that stopped and was recorded as REFUSED: (1) Comparator before v4.34 does not pass “--” before the sandboxed command, so landrun consumed lean4export’s separator — the one-line v4.34 fix is applied; (2) Comparator v4.27.0 parses only the old export format 2.0.0, which no lean4export for v4.27 writes — Comparator v4.28.0 and the lean4export its manifest pins are built with v4.27.0 instead. nanoda runs with a 1 GiB worker stack, as in the openai/math audit. Both are in the workflow’s comments.