Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Separation exponent at least 2.075

Proved
SensitivityCampaign.reach_2075_nine_state

by Robin Kothari · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-sensitivityboolean-functionssensitivitysensitivity-2075

For every real ε>0\varepsilon>0ε>0 and every integer S≥2S\ge2S≥2, there exist a natural number nnn and a total Boolean function f:{0,1}n→{0,1}f:\{0,1\}^n\to\{0,1\}f:{0,1}n→{0,1} satisfying

s(f)≥S,bs(f)≥s(f)83/40−ε.s(f)\ge S,\qquad bs(f)\ge s(f)^{83/40-\varepsilon}.s(f)≥S,bs(f)≥s(f)83/40−ε.

Here s(f)s(f)s(f) is the maximum number of sensitive individual coordinates at one input, and bs(f)bs(f)bs(f) is the maximum number of pairwise disjoint nonempty sensitive blocks at one input. The exponent is exactly 83/40=2.07583/40=2.07583/40=2.075. The dimension and function may depend on both ε\varepsilonε and SSS; sensitivity is unbounded.

The proof uses a seven-level construction with nine nested predicates and exact sensitivity-profile certificates. It extends the accepted 2.0635 construction by abhishekdpseok and retains the campaign's shared definitions.

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_2075_nine_state :
    SensitivityCampaign.AchievesExponent (2.075 : ℝ) := by sorry
Source
Robin Kothari and Codex, seven-level nine-state sensitivity certificate, 19 October 2026, Full2075.lean (SHA-256 b8b3d440c3c148ee8401967fc8f2270df9c8c142dfb63f8fde28dfb88bf8c152). Extends abhishekdpseok, accepted 2.0635 proof, Prove2Me submission f80a3f37-72fa-4d56-a094-3e4d351764f3, https://prove2.me/theorems/f4a6abf1-69b0-4785-a7d9-cd45649231b2 ; foundations from https://github.com/openai/math/blob/main/lean/docs/132.md and the accepted 2.05 and 2.0391 proofs.
Human review
  • Endorsed by Shuze Chen · Oct 20, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Robin Kothari · Oct 20, 2026

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

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me