Erdős problem 690 took months of harness engineering. These six took five days, and almost all of the work went into the prompt. Each one states exactly what a full proof has to establish, names the traps, and sends adversarial agents at every candidate argument. We attempted about thirteen problems, so a little under half worked out. Every proof is posted on the erdosproblems.com forum for public attack, and the prompt that produced it is published next to it.
Proposed solutions, published for attack rather than certified. Source, prompts and Lean formalisations are at github.com/ShouqiaoW/erdos.
- 390An exact asymptotic for the least largest factor of a factorisation of n!Number Theory
- 486A sieve whose survivors have no logarithmic densityNumber Theory
- 536Sets with no three equal pairwise least common multiples have density zeroCombinatorics
- 788The trade-off function is a square root, up to no(1)Additive Combinatorics
- 1002Rotation discrepancy converges to a Cauchy lawEquidistribution
- 1038The exact infimum of a polynomial sublevel setApproximation Theory