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

5. erdos-theorems erdos-theorems Public

   79 kernel-verified Lean 4 declarations across 15 open Erdos problems, every one with a clean axiom footprint

   Lean

6. erdos203-obstruction-calculus erdos203-obstruction-calculus Public

   An exact subgroup-obstruction calculus for two-generator exponential congruence problems, with applications to Erdos-Graham #203 and a precise Kummer non-concentration criterion

   TeX