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. lean-in-lowell lean-in-lowell Public

   Lean courses at UMass Lowell

   Lean 2 1

3. dir24-isoperim dir24-isoperim Public

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

   Python 1

4. microlean microlean Public

   A minimalistic variant of Lean written in Zig

   Zig

5. lean-spherical lean-spherical Public

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

   Lean 2 1

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