Popular repositories Loading

1. 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

2. 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

3. 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

4. alderwatch alderwatch Public

   TypeScript

5. erdos152 erdos152 Public

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

   HTML

6. lean-semantic-blades lean-semantic-blades Public

   A 33-blade deterministic semantic certification gate for autoformalized mathematics, with full output over 160 Erdos problem formalizations

   Python