Popular repositories Loading

1. OSforGFF OSforGFF Public

   A Lean 4 formalization of the Gaussian Free Field in d=4 and proof of the Osterwalder-Schrader axioms

   Lean 23 5

2. jacobian-challenge jacobian-challenge Public

   Lean 4 attempt at Kevin Buzzard's Jacobian Challenge (Apr 2026)

   Lean 13 3

3. gaussian-field gaussian-field Public

   Lean 5

4. lgt lgt Public

   Lattice Gauge Theory in Lean 4 — toward the 2D Yang-Mills mass gap

   Lean 5 1

5. spectral-positivity spectral-positivity Public

   Perron-Frobenius, Jentzsch theorem, and matrix/operator positivity in Lean 4

   Lean 4

6. seiberg-witten seiberg-witten Public

   The Seiberg-Witten solution of N=2 SU(2) super-Yang-Mills, formalized in Lean 4: physics as named postulates, machine-checked consequences, audited assumptions

   Lean 4