rrma erdos solver

solver.txt

From Table 1 of the paper. Here they are ranked by how well they fit the current RRMA setup:

  ---
  Cluster 1 — Density (reuse #125 infrastructure directly)

  ┌─────────┬──────┬──────────────────────────────────────────────────────────────┬──────────────────────────────────┐
  │    #    │ Year │                          Statement                           │            Technique             │
  ├─────────┼──────┼──────────────────────────────────────────────────────────────┼──────────────────────────────────┤
  │ 125     │ 1996 │ lowerDensity(A+B) = 0 for base-3/4 digit sets                │ Dirichlet + inductive thinning ← │
  │         │      │                                                              │  running                         │
  ├─────────┼──────┼──────────────────────────────────────────────────────────────┼──────────────────────────────────┤
  │ 741(i)  │ 1994 │ If A+A has upper density, ∃ decomposition A=A₁⊔A₂ with both  │ Upper density case analysis      │
  │         │      │ pieces positive upper density                                │                                  │
  ├─────────┼──────┼──────────────────────────────────────────────────────────────┼──────────────────────────────────┤
  │ 741(ii) │ 1994 │ ∃ basis A of order 2 with A₁+A₁, A₂+A₂ bounded gaps for all  │ Explicit rapidly growing         │
  │         │      │ splits                                                       │ sequence construction            │
  └─────────┴──────┴──────────────────────────────────────────────────────────────┴──────────────────────────────────┘

  lowerDensity, upperDensity, liminf infrastructure from #125 carries over directly. Run these next — cheapest seed.

  ---
  Cluster 2 — CRT / Block construction

  ┌────────┬──────┬───────────────────────────────────────────────────────────┬──────────────────────────────────────┐
  │   #    │ Year │                         Statement                         │              Technique               │
  ├────────┼──────┼───────────────────────────────────────────────────────────┼──────────────────────────────────────┤
  │ 12(i)  │ 1970 │ ∃ A ⊂ ℤ⁺ with a∤(b+c) and |A∩[1,N]|/√N > δ > 0 infinitely │ CRT + 3-AP avoiding sets             │
  │        │      │  often                                                    │                                      │
  ├────────┼──────┼───────────────────────────────────────────────────────────┼──────────────────────────────────────┤
  │ 12(ii) │ 1970 │ Same divisibility constraint but |A∩[1,N]| ≫ N^{1-ε}      │ CRT + 3-AP avoiding sets             │
  ├────────┼──────┼───────────────────────────────────────────────────────────┼──────────────────────────────────────┤
  │ 26*    │ 1995 │ ∃ A with upperDensity(A+k) < 1-¼ for all k                │ CRT + increasing primes + density    │
  │        │      │                                                           │ bounds                               │
  └────────┴──────┴───────────────────────────────────────────────────────────┴──────────────────────────────────────┘

  Same proof skeleton — CRT is well covered in Mathlib. These three can share one blackboard.

  ---
  Cluster 3 — Harder / different tooling

  ┌──────┬──────┬────────────────────────────────────────────────────────┬───────────────────────────────────────────┐
  │  #   │ Year │                       Statement                        │                 Technique                 │
  ├──────┼──────┼────────────────────────────────────────────────────────┼───────────────────────────────────────────┤
  │ 138* │ 1981 │ Van der Waerden numbers: W(k+1)-W(k) → ∞               │ Greedy coloring + monochromatic           │
  │      │      │                                                        │ intersection                              │
  ├──────┼──────┼────────────────────────────────────────────────────────┼───────────────────────────────────────────┤
  │ 152  │ 1994 │ Large Sidon sets contain many isolated points in A+A   │ Interior point bounds + quadruples        │
  ├──────┼──────┼────────────────────────────────────────────────────────┼───────────────────────────────────────────┤
  │ 846  │ 1992 │ ∃ infinite A with no finite union of non-collinear     │ Fast-growing sequence + algebraic map     │
  │      │      │ subsets                                                │                                           │
  └──────┴──────┴────────────────────────────────────────────────────────┴───────────────────────────────────────────┘

  These need Ramsey theory, Sidon set lemmas, or algebraic geometry tooling — less Mathlib coverage, harder seeds.

  ---
  Recommended order:

  #125 (now) → #741(ii) → #741(i) → #12(i) → #12(ii) → #26* → #152 → #138* → #846

  741(ii) is the immediate next — it's a construction proof (explicit sequence), easiest to formalize, and the density
  infrastructure is already built. Seed it while #125 is still running.