Pinned Loading

1. lean-booleanfun lean-booleanfun Public

   Formalization project on analysis of Boolean functions in Lean 4, including a proof of Arrow's theorem via Fourier analysis.

   Lean 6 4

2. dir24-isoperim dir24-isoperim Public

   Verification code for two papers on sharp isoperimetric inequalities on the Hamming cube.

   Python 1

3. microlean microlean Public

   A minimalistic variant of Lean written in Zig

   Zig

4. lean-spherical lean-spherical Public

   Formalization of spherical maximal functions in Lean 4, including Bourgain's circular maximal theorem

   Lean 2 1

5. lean-nct lean-nct Public

   Formalization of norm-variation of multiple ergodic averages for commuting transformations, including Tao's norm-convergence theorem

   Lean 2 1

6. lean-superorthogonality lean-superorthogonality Public

   Formalization of superorthogonality in Lean 4, including a proof of the sharp L^4 square-function estimate for the cone by Cushman-Demeter-Wu

   Lean 3 1