Can a greedy sequence of primes run forever?
I’m Syn. This is my working notebook for an attack on Erdős 472—models proposing ideas, code trying to break them, Lean checking the semantic core, and me deciding what survives.
I have not solved it. The best trajectory has passed one million verified steps, but a finite run is still finite.
The beginning of the singleton [7] orbit
q = 6x + 1
The rule
Start with a finite increasing list of primes. At each step, take the current last term qn and inspect
for every earlier term qi. Append the least prime candidate. If they are all composite, stop.
What has survived scrutiny
Ideas the project has killed
- 01
Static certificates. CRT can assign fresh blockers to any fixed finite shell.
- 02
Scheduled winners. They hide a thin infinite-prime conjecture.
- 03
Unsigned factor counts. They do not cross the sieve parity barrier.
- 04
Finite memory. Rich finite behaviour can still be programmed to terminate.
Where the proof stops
The current candidate is a growing-age selector built from the actual birth history of the singleton [7] orbit. After filtering small prime factors, the remaining obligation is one centered rough/semiprime estimate.
F280 / not yet provedR cube-root-rough mass
S rough semiprime mass
Π prime mass
The right side is a positive flat prime reserve. If the two errors on the left stay smaller, selected prime mass is positive and a hypothetical terminal row cannot exist. That uniform inequality is the missing mathematics.
Centered budget against failure threshold 1
38,692 rows audited · ranks 1,309–40,000
rank 1,755 · margin 0.076771292
Finite means finite. The audit found no failure in this interval. It does not prove the next row.
How I’m working
AI is useful here when it behaves like a restless collaborator: propose a precise claim, write the falsifier, search for the smallest counterexample, and keep the analytic debt visible.
Code checks finite worlds. Lean checks deterministic implications. Primary papers supply named analytic inputs. I remain responsible for deciding what the evidence supports and what gets published.
Primary sources first.