Prove2Me

Separation exponent at least 2.13

Proved
SensitivityCampaign.reach_2_13

by marwahaha · Oct 20, 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.13−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.reach_2_13 :
    SensitivityCampaign.AchievesExponent (2.13 : ℝ) := by sorry
Source
https://github.com/bigospeedrun/site/issues/2
Human review

  • Endorsed by Shuze Chen · Oct 20, 2026

    Confirmed by the moderator at approval.

  • Endorsed by marwahaha · Oct 20, 2026

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

View graph