Popular repositories Loading

1. erdos-graham-203-411-corpus erdos-graham-203-411-corpus Public

   Full working corpus for Erdos-Graham 203 and 411: Lean proofs, GPU certificates, the omega-7 kill tree, and 19 papers. Both problems remain OPEN.

   Lean 1

2. erdos710-descent-and-1044 erdos710-descent-and-1044 Public

   An observed prime-descent law for Erdos 710 with five primes held out as a live test, five sealed Hall theorems, and a closed form for the Erdos 1044 extremal family

   Lean 1

3. erdos902 erdos902 Public

   Lean 4 formalisation of the classical bounds for Erdős #902 (Schütte), including the Szekeres–Szekeres lower bound; kernel-checked. Problem remains open.

   Lean

4. erdos203 erdos203 Public

   Erdős–Graham #203: coset-cover attack corpus. Exact structural results, replayed finite obstructions (N=5040 pool kill, overlap tax), and search engines. Problem remains open.

   Python

5. erdos411 erdos411 Public

   Erdős–Graham #411 (r=2): the Steinerberger–Hercher bridge, the base-6 cascade (axiom-free Lean), and the omega-ladder; no exceptional prime below 1.33e14. Residual gap open; retraction preserved.

   Lean

6. erdos-160-problem-statements-in-lean erdos-160-problem-statements-in-lean Public

   160 Lean 4 formalizations of open Erdos problem statements, published with their full defect audit including the 72 the gate rejected

   HTML