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

A formalized proof of Carleson's theorem in Lean

Lean 4 programming language and theorem prover

The math library of Lean 4

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

FLINT (Fast Library for Number Theory)

Python bindings for Flint and Arb