roos-jBooleanFun0.1.0

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

Analysis of Boolean functions in Lean

Lean

This is a project formalizing some basic definitions and results in the analysis of Boolean functions using Lean 4, largely following the book Analysis of Boolean functions by Ryan O'Donnell.

Main results formalized so far:

  • Plancherel's theorem for the Walsh-Fourier transform
  • L² Poincaré inequality
  • Blum-Luby-Rubinfeld linearity testing
  • a version of Arrow's theorem

Installation

  1. Install Lean 4 and dependencies as explained here.

  2. Clone this repository using

     git clone https://github.com/roos-j/lean-booleanfun.git

and open it in VS Code (more instructions here).

Palomar registration

The formalization of Arrow's theorem in this repository is registered in Palomar as PALOMAR-2026-09-01-000011. Palomar is a public, searchable registry of Lean formalizations whose proofs have been machine-checked. Each entry points to an immutable version of a public repository and records the exact formal statement that was checked, its dependencies, the result of the proof check, and the findings of a documented editorial review.

Future goals

  • hypercontractivity, Bonami lemma
  • KKL theorem
  • Bobkov's two-point inequality
  • Talagrand's isoperimetric theorem
  • FKN theorem

Note: the central limit theorem will be needed eventually; currently not in Mathlib

Previous formalizations of Arrow's theorem

Arrow's theorem has been formalized before (and in more general formulations):

These formalizations use direct combinatorial arguments of John Geanakoplos.

The formalization in this project uses Gil Kalai's Fourier-analytic approach. It formalizes the version of Arrow's theorem stated in Sec. 2.5 of Ryan O'Donnell's book and follows the exposition given there.

AI Statement

As of the current commit, this repository is still entirely human-generated. Most of the code was written as a Lean learning exercise in Fall 2024 and has only been refactored and updated in minor ways since. However, AI may be used in the future and in particular, sensible machine-generated contributions are welcome.