Popular repositories Loading

1. Arda Arda Public

   Machine-checked progress on the Brualdi-Goldwasser (1984) Laplacian-ratio maximizer for trees (Lean 4 + Mathlib, no sorry) + Telperion, a sympy-to-Lean certificate pipeline

   Lean 1

2. brualdi-goldwasser brualdi-goldwasser Public

   Which tree maximizes per(L)/prod deg? A complete answer for every n, kernel-checked in Lean 4 (Brualdi-Goldwasser 1984).

   Lean

3. qrh-debruijn-newman qrh-debruijn-newman Public

   A kernel-checked bound Lambda <= 9/32 for the de Bruijn-Newman constant from OpenAI's quasi-Riemann hypothesis (Lean 4, Comparator-judged). Not RH.

   Lean

4. newman-lambda-nonneg newman-lambda-nonneg Public

   Newman's conjecture Lambda >= 0 for the de Bruijn-Newman constant, kernel-checked in Lean 4 along Dobner's proof (Arda dbn island); paper, sources, verification trail

   Lean

5. mathlib4 mathlib4 Public

   Forked from leanprover-community/mathlib4

   The math library of Lean 4

   Lean