Four days ago the lab's Erdős wing graded a machine's homework — OpenAI's three-page Cycle Double Cover proof — and returned a deliberately narrow verdict: corroborated, not promoted. That proof was a construction, so we could execute it on 409 graphs and watch it hold. This week a different proof-shaped object arrived, and it invites a different — and, we think, more inviting — kind of scrutiny: the kind you can carry out yourself, with a pencil.
On July 13th a claimed solution to Erdős Problem 793 was posted to the problem's comment thread — a five-page note, credited by its author to GPT-5.6 Sol Ultra. The problem remains marked open on erdosproblems.com, and the note is unrefereed. What makes it approachable rather than daunting is that the argument is elementary: no 409-graph battery, no Lean kernel required to begin. If you recall the prime number theorem and how to sum a geometric series, you can read the note and judge for yourself whether it holds. So this entry is two things at once — our own check, and an invitation to run yours.
The problem, in plain words
Fix a whole number n and consider the integers from 1 to n. The goal is the largest subset you can assemble under a single rule: no number in the subset divides the product of two others — where the "two others" may be the same number, used twice. That final clause is subtle, and it does real work; keep it in view.
The primes are already a large legal subset — roughly π(n) of them — and no prime divides a product of two other members, for elementary reasons. So the primes are the easy floor, and the real question lives in the second wave: how many further members can you admit beyond the primes? Erdős showed this extra wave has size on the order of n^{2/3} / (log n)², but he could only trap its constant between two values, never pin it exactly. Problem 793 is precisely that gap, posed as a clean yes-or-no:
Is there a single constant C for which F(n) = π(n) + (C + o(1))·n^{2/3}/(log n)²?
The claim
Yes — and the constant is C = 27/2. The note resolves it the way problems of this shape usually yield: a matching upper and lower bound that pincer the constant from both sides. The upper bound builds an efficient "factor dictionary" and shows that no legal subset can outnumber it; its two non-trivial shelves count 9/2 and 9, and 9/2 + 9 = 27/2. The lower bound works in the other direction and explicitly constructs a near-maximal set from carefully chosen prime triples, packed by an explicit graph edge-colouring; a geometric series delivers the same 27/2 from below. The two values meet in the middle. That is the whole of the argument — and it is a genuine, elegant refinement of Erdős's own 1938 method, not a hallucination in the shape of a proof.
How we checked it
The same discipline as last time, turned on someone else's work: not "does this look right" but "try to break it." Two independent adversarial re-derivations, one per half of the proof, each instructed to refute rather than confirm, and to reconstruct every constant from scratch rather than nod along to the paper's. Plus one check of our own design (below).
A caveat, honestly updated. Last time, both careful reads of the CDC proof came from the same model family — two GPTs, which is one telescope pointed twice, not two independent looks. This time genuinely differs: the proof is GPT's; the checkers are Claude — a different family, a different lens. That is a real gain in independence over the previous grade. It remains, however, a machine reading a machine: not a human referee, and not the kernel. Hold that distinction — it is load-bearing at the end.
What we found
It holds. Every load-bearing step re-derived and confirmed — the factor-dictionary injection, the prime-counting sums that yield 9/2 and 9, and the geometric series that yields 27/2 from below. The delicate clause — that the "two others" may coincide — is exactly where an elegant argument is tempted to take a shortcut, and here it is handled: squaring a single element can supply at most one of a target's three prime factors, so the case stays closed.
| Question | Verdict |
|---|---|
| The note states the real problem and claims a specific constant (C = 27/2) | PASS |
| Upper bound: does the factor dictionary really cover every number ≤ n, and count to 27/2? | RE-DERIVED |
| Lower bound: is the prime-triple construction actually legal, incl. the doubling clause? | RE-DERIVED |
| Consistency: does the upper 27/2 truly sit above the lower 27/2 (no hidden factor)? | PASS |
| Peer review, expert verification, or a kernel-checked formal proof | NOT ESTABLISHED |
The one flaw we found is cosmetic. In the lower-bound argument, a single case — what if the number in question is itself one of the leftover primes? — is true but never written down. It closes in one sentence (a leftover prime divides no triple-product and no other prime, so it is safe). A hostile referee will note its absence; it is not a gap in the mathematics.
The check we added ourselves is the part most worth borrowing. A matching-constant proof carries an elegant failure mode: should the upper bound's "dictionary" quietly overlap itself too much, its true size shrinks — and a shrunken upper bound can fall below the lower bound, at which point the two halves contradict and the result collapses. So rather than take the note's word that the shelves are disjoint, we counted the overlaps ourselves. They are negligible; the bounds honestly meet. That test does not appear in the note, and it is the single most likely place a mistaken 27/2 would have failed.
And we checked it by machine, too
Careful reading is one instrument; a computer is another, and they fail in different ways — so we used both. We built the note's lower-bound construction directly — the linear hypergraph of prime triples, assembled from a proper edge-colouring exactly as described — and verified by exhaustion, instance after instance, that the resulting set is genuinely strongly 2-primitive: no member divides the product of two others, with the squaring case and the leftover-prime case explicitly included. Pointed instead at a deliberately non-linear version of the same construction, the checker immediately produces a violation — which is what makes its passes worth anything. And the note's constants — the 9/2, the 9, the cell-weight series collapsing to 3/2 — reproduce under an independent prime sieve. This is corroboration, not proof: no finite computation can pin an asymptotic constant, and the honest caveat is that the second-order terms converge as slowly as the prime number theorem. But it is a mechanical check anyone can reproduce, not a verdict you are asked to take on faith.
Why we won't stamp it “verified”
In this lab, verified is a reserved word: it means the Lean 4 kernel accepted a proof with zero axioms — an exit code, not a model's opinion. This note has neither a formalization nor a referee, so the word is not ours to use, and we won't. The honest grade is the same shape as before: independently checked, holds up — not settled. “Settled” would mean the number-theory community signs off, or a kernel receipt exists whose statement has been audited against the problem. Neither exists yet. Two developments would settle it: publication and refereeing, or a Lean formalization of the argument. One would overturn it: a single number the factor dictionary fails to cover, or a triple that breaks the doubling clause.
Now you try
The invitation is sincere. This proof is small and elementary enough that you need no one — not us, not any model — standing between you and the truth of it. Read the note alongside the problem, bring a pencil, and aim your skepticism at the three places we attacked:
1. The dictionary's coverage. The upper bound rests entirely on the claim that every number up to n factors into two dictionary entries. That sentence is where arguments of this kind most often leak. Try to find the number that doesn't.
2. The doubling clause. Because "a number may not divide the product of two others" permits those two to be the same number, every step must survive squaring. Walk the lower-bound construction and confirm that no triple-product divides another element squared.
3. The consistency test. Satisfy yourself that the upper 27/2 truly stays strictly above the lower 27/2 — that no factor of two was dropped on either side. If one was, the constant is wrong even though both halves "look" like 27/2.
Find a genuine crack in any of those and it is front-page news in this journal — the same standing offer we made for the snark probe. This is the oldest pleasure in mathematics: a short argument about prime numbers is a small democracy. It does not matter whether a frontier model or a person wrote it — it is either true or it isn't, and you are permitted to check. The machine may have found a door; whether it opens onto anything is something you can decide for yourself.
This is one assay from the lab's Erdős wing — a small engine for checking, and in time helping to make, machine-assisted mathematics, one honest receipt at a time. That is what we are doing here. Trust the receipt. Then try to break it.