I promised to revisit nine AI mathematics claims on 20 October. I returned to them on 28 October, after publishing an article about missing the deadline.

Then I found that someone else had published a formal replay of the proofs on 20 October.

Apparently, my calendar was not essential infrastructure for mathematics.

The original investigation, Nine Became Eight, followed nine AlphaProof Nexus result claims. They covered seven Erdős problem numbers: some were separate parts, others particular variants. One result was excluded from my strict novelty count because an older theorem already implied its conclusion. The remaining eight were provisional.

TID record and evidence: Problem Frontier Baseline — 2026-07-20 →

The late follow-up found three developments worth separating.

The checking acquired more layers

The AlphaProof Nexus paper was published in Science on 8 October, according to the publisher's metadata. I could verify that publication record; I could not directly inspect the final journal text and supplement.

Carlos Toledo's public audit added a different kind of evidence. It reports replaying the published Erdős proofs, plus the separately corrected upper-density proof for 741(i), through Lean and the independently written Nanoda kernel. I matched the solution hashes for our nine cases and checked the corresponding successful GitHub runs and jobs. I did not run that toolchain myself.

This checks whether a formal argument proves the specified formal statement. Choosing the right statement, establishing its historical novelty and reviewing an informal explanation still require their own work.

That distinction remains visible in our cases. The old repository's file named 741(i) proves a different density interpretation from the corrected result. Formal Conjectures made upper density its main formulation in August. The corrected proof was already available separately in April.

One problem moved beyond our old result

The result I reviewed in July for problem 138 concerned the difference between consecutive van der Waerden numbers. Since then, an August preprint and OpenAI's October mathematics release have addressed stronger growth questions.

In the records I checked on 28 October, Formal Conjectures marks the root-growth question solved and links to the new Lean material. The captured community database still labels the parent problem open. Another question, about the ratio of consecutive terms, remains open in that Formal Conjectures revision.

A label saying “open” can therefore conceal progress. A label saying “solved” needs a sentence explaining which question was answered.

The newer work has its own authors, evidence and dates. It does not become another discovery by the system I investigated in July.

Eight is still provisional

In the sources checked, I found no newly located withdrawal or refutation of the nine precisely scoped results. That is a bounded search finding. I have not independently peer-reviewed all the mathematics or completed a new exhaustive priority audit.

All nine proof artifacts in our review and their accompanying prose PDFs match the July hashes. The previously documented defects in those unchanged files remain relevant. The older implication behind 846 also remains: another successful formal replay does not restore its place in the strict novelty count.

For these cases, the public record now contains journal publication, external replay, clearer specifications and further research. Those are useful, different contributions to checking a claim. A headline total compresses them too aggressively.

I have prepared a dated TID update recording both the missed review and this narrower follow-up. The July payload stays intact. The broader quarterly comparison, including OEIS reconciliation and comparable registry changes, is still incomplete. I am keeping scheduled tracking paused.

I was eight days late. This time, there is also a record of what I checked.

— Dennis Hedegreen, trying to see the structure

Sources and the dated record