Sensitivity Theorem in Lean 4

This repository formalizes the sensitivity lower bound for Boolean functions in Lean 4, building on Mathlib's formalization of Huang's hypercube lemma in Archive/Sensitivity.lean.

Main Result

For any Boolean function f : {0,1}^n -> {0,1} with multilinear degree d >= 1,

sqrt(d) <= s(f)

where s(f) is the sensitivity of f.

In Lean:

• Sensitivity.sensitivity_ge_sqrt_degree
• Sensitivity.degree_le_sensitivity_sq

The current codebase is proof-complete (no sorry).

File Layout

Sensitivity/
  Defs.lean          -- Boolean functions, bit flips, sensitivity
  Basic.lean         -- Basic sensitivity lemmas and symmetries
  Multilinear.lean   -- Mobius coefficients and degree
  Subcube.lean       -- Restriction to subcubes and coefficient preservation
  Parity.lean        -- Parity identities and imbalance lemma
  HuangBridge.lean   -- Finset bridge to Mathlib's huang_degree_theorem
  Main.lean          -- The sensitivity lower bound sqrt(deg) <= s
  Consequences.lean  -- Corollary deg <= s^2

Proof Outline

1. Use a nonzero top Möbius coefficient as a degree witness.
2. Restrict to a subcube that preserves this coefficient.
3. Derive a parity-sign imbalance on the restricted cube.
4. Apply Mathlib's Huang theorem to obtain many same-class neighbors.
5. Convert these neighbors into sensitive coordinates and lift back to f.

Build

lake update
lake build

Acknowledgments

This formalization was inspired by the lean-sensitivity project by the Lean community, which formalized Huang's proof of the Sensitivity Conjecture shortly after its announcement in 2019. That formalization was later incorporated into Mathlib as Archive.Sensitivity, which we use here as the foundation for bridging to Huang's hypercube eigenvalue argument.

References

• Hao Huang, Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture, Annals of Mathematics 190(3), 949-955, 2019.
• Noam Nisan and Mario Szegedy, On the degree of Boolean functions as real polynomials, Computational Complexity 4, 301-313, 1994.
• Lean community, lean-sensitivity, 2019. Formalization of Huang's proof in Lean, now part of Mathlib.