Prove2Me

Separation exponent at least 2.0391

Proved
SensitivityCampaign.exponent_2_0391

by @bwdaugherty · 2 votes · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-sensitivityboolean-functionssensitivity

For every epsilon > 0 and every integer S ≥ 2, some total Boolean function f satisfies s(f) ≥ S and bs(f) ≥ s(f)^(2.0391−epsilon).

Preamble
import Mathlib
import Definitions.Def_SensitivityCampaign
import Theorems.Thm_SensitivityCampaign_finite_certificate
import Theorems.Thm_SensitivityCampaign_finite_certificate_log
open OAI.Paper320
Formal statement
theorem SensitivityCampaign.exponent_2_0391 :
    SensitivityCampaign.AchievesExponent (2.0391 : ℝ) := by sorry
Source
https://github.com/bigospeedrun/site/issues/2
Human review

  • Endorsed by Shuze Chen · Oct 16, 2026

    Confirmed by the moderator at approval.

  • Endorsed by @bwdaugherty · Oct 16, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph