Popular repositories Loading

1. palomar-ingham palomar-ingham Public

   Palomar registry entries: Ingham's equivalence and primes in arithmetic progressions (Lean v4.35.0)

   Lean 2 1

2. morley-smith-formal morley-smith-formal Public

   Lean-verified results by Richard Morley-Smith: congruences between modular forms (Lean 4, Mathlib, Comparator-checked)

   Lean 2 1

3. fugue-formal fugue-formal Public

   Machine-checked Lean 4 / Mathlib proofs from the HSLN exploration: Θ_E8 = E₄, E8⊕E8 and Witt's D16⁺, τ(n) ≡ σ₁₁(n) mod 691, two squares, L(1,χ₋₄) = π/4, Euler products; 103 audited theorems, no sorry

   Lean 1

4. fugue-formal-pnt fugue-formal-pnt Public

   Ingham's theorem in Lean 4: ζ zero-free right of θ ⟺ ψ(x) = x + O(x^(θ+δ)); RH ⟺ square-root error term. No sorry.

   Lean 1

5. fugue fugue Public

   HSLN / Fugue: handover and evidence-graded audit of the June 2026 corpus; index of the formalisation and archive repositories

   Python 1

6. fugue-exploration fugue-exploration Public

   The June 2026 HSLN exploration, tidied: scripts with five-part headers (what is computed, what is proved and its Lean name, what is not claimed, how it was found), 47 regenerated figures, family notes

   Python 1