Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Separation exponent at least 2.1308255793978239…2.1308255793978239\ldots2.1308255793978239…

Proved
SensitivityCampaign.reach_source_q5_best_3738277295413674

by yousofy · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-sensitivityboolean-functionssensitivity

Set

α=log⁡(1522813785050025472152230187890625)log⁡(3738277295413674)=log⁡(140558)log⁡(3738277295413674)=2.1308255793978239476….\alpha=\frac{\log(1522813785050025472152230187890625)}{\log(3738277295413674)}=\frac{\log(14055^8)}{\log(3738277295413674)}=2.1308255793978239476\ldots.α=log(3738277295413674)log(1522813785050025472152230187890625)​=log(3738277295413674)log(140558)​=2.1308255793978239476….

For every real ε>0\varepsilon>0ε>0 and every natural number 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} with

s(f)≥S,bs⁡(f)≥s(f)α−ε.s(f)\ge S,\qquad \operatorname{bs}(f)\ge s(f)^{\alpha-\varepsilon}.s(f)≥S,bs(f)≥s(f)α−ε.

Here s(f)s(f)s(f) is the maximum number of sensitive singleton coordinates over all inputs, and bs⁡(f)\operatorname{bs}(f)bs(f) is the maximum number of pairwise disjoint nonempty sensitive blocks over all inputs. This is the campaign's unchanged AchievesExponent predicate at the exact logarithmic value. The decimal is an approximation. The already accepted primitive theorem proves the same quantified assertion and a strict comparison with the preceding five-tolerance bound.

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_source_q5_best_3738277295413674 :
    SensitivityCampaign.AchievesExponent (Real.log (1522813785050025472152230187890625 : ℝ) / Real.log (3738277295413674 : ℝ)) := by sorry
Source
Exact campaign-template form of https://prove2.me/theorems/01bb63ef-ced2-4ae9-8b81-b5ed295526c6, accepted submission a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. Shared definitions and template from https://prove2.me/campaigns/block-sensitivity-vs-sensitivity. Earlier OpenAI and Robin Kothari/Codex attribution is retained in the accepted source. New construction: yousofy with Codex.
Human review
  • Endorsed by Shuze Chen · Oct 21, 2026

    Confirmed by the moderator at approval.

  • Endorsed by yousofy · Oct 21, 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