Stars
Lean Formalization of Endpoint Estimates for Stein's Purely Quadratic Carleson Operator
Formalization of superorthogonality in Lean 4, including a proof of the sharp L^4 square-function estimate for the cone by Cushman-Demeter-Wu
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
Verification code for two papers on sharp isoperimetric inequalities on the Hamming cube.