openmath.dev
Esc

Loading…

↑ ↓ to move↵ to open

Appearance
Appearance
← Problems

Probability · Conjecture

Feige’s probability conjecture

How small can P(S<ES+1)\mathbb P(S<\mathbb ES+1) be for a sum S of independent nonnegative random variables whose individual means are at most one?

ProvedOpenMath assessment · Oct 13, 2026
Frontier 1 report →
Cite & export
Open this versionExport record · JSONRecord detailsReport a correction
Use with an agent

Earlier version 1 of this page. View current →

Overview

Known

The unit-slack question is proved in two separately credited July papers, with finite-dimensional optimality reported complete in Lean. A later Samuels paper proposes the full sharp formula for arbitrary positive deviations.

Latest

Precise statement

Fix a positive finite integer n. The variables X₁,…,Xₙ are independent, nonnegative and integrable with E Xᵢ ≤ 1, and S = Σᵢ Xᵢ. The event is strictly below the mean plus one; a mass at the threshold is excluded. The finite-dimensional sharp constant and the limit over all n are different bounds. Other positive deviations δ have their own Claims.

Question paraphrased by OpenMath. Original wording is available in the sources.

Landscape

Figures and explorable examples. Selecting a statement opens its exact wording.

The sharp constant by dimension

The sharp constant for n variables, (n/(n+1))ⁿ, falls towards 1/e as n grows; earlier universal lower bounds sit well below it.

00.10.20.30.40.510203040number of variables nsmallest P(S < E S + 1)(n/(n+1))ⁿ, sharp1/e, the limit0.1798 (2020)1/8 (2010)1/13 (2004)(n/(n+1))ⁿ, sharp1/e, the limit0.1798 (2020)1/8 (2010)1/13 (2004)

Drawn for n ≤ 40. The values are exact; the theorems for every n and for 1/e are the linked statements. Garnett’s approximately 0.14 (2020) is not drawn: the source gives it only approximately.

Dataset feige-sharp-constant v1 · (n/(n+1))ⁿ computed as exact rationals for n = 1, …, 40 and checked to decrease; the flat lines are the cited constants 1/e, 0.1798, 1/8 and 1/13. Software: python 3.12.15. Exact rationals, stored as floating point. SHA-256 8273cb9c4adb… · Download JSON

Data
SeriesPointsLast value (number of variables n = 40)
(n/(n+1))ⁿ, sharp400.37243062369780505
1/e, the limit400.36787944117144233
0.1798 (2020)400.1798
1/8 (2010)400.125
1/13 (2004)400.07692307692307693

Visual setup

Why the strict threshold matters

Three independent variables, each 0 or 4, attain the finite-dimensional unit-slack bound (3/4)³ = 27/64.

Reading boundary. This exact extremizer demonstrates attainable equality. The universal lower bound for arbitrary distributions requires the cited proof.

Why the strict threshold mattersThe sum has values 0,4,8,12 with probabilities 27/64,27/64,9/64,1/64. Its mean is three, so mean plus one is four. The atom at four is excluded from the event.n = 3 · each Xᵢ is 0 or 4P(Xᵢ = 4) = 1/4 · E Xᵢ = 1Strict threshold 4027/64427/6489/64121/64P(S < 4) = 27/64
Inspect fixed-dimensional optimality● Proved under stated assumptionsRead the strict event conventionQuestion scope

The point at the threshold does not count. Select the bound for its hypotheses and formal evidence.

Text version

The sum has values 0,4,8,12 with probabilities 27/64,27/64,9/64,1/64. Its mean is three, so mean plus one is four. The atom at four is excluded from the event.

The three variables are independent and identically distributed for this example. Identical distributions are not required by the theorem.

  1. Inspect fixed-dimensional optimality

    Proved

    The optimal bound for a fixed number of variables

    Both July arguments support the same mathematical assertion. The pinned Lean declaration formalizes this fixed-dimensional optimality statement.

    The optimal bound for a fixed number of variables →

  2. Read the strict event convention

    Proved

    The dimension-free unit-slack inequality

    The conventional unit-slack conjecture. The stronger finite-n theorem yields this bound and approaches 1/e as n grows.

    The dimension-free unit-slack inequality →

Sources & review

Authored by OpenMath source curation on 2026-10-13 (AI-assisted curation). Independent review of this visual explanation is pending; linked assertions and relationships have their own assessments.

Results

The question 1

Bounds 1

Proposed 1

  • Proposed
    The later proposal for every positive deviation

    Ling’s later Corollary 1.3 proposes the fully sharp formula; it is not part of the linked unit-slack Lean proof.

    Ling 2026

Conditional implications 1

  • Proved
    The universal constant is a limit across dimensions

    Finite-dimensional equality examples attain their own larger constants.

    Fu et al. 2026

Variants and analogues 1

  • Proved
    The July bounds in two deviation ranges

    The first branch is a lower bound, without a sharpness claim.

    Fu et al. 2026

Connections

Analogues and related questions 1

Consequences 1

Assuming The optimal bound for a fixed number of variablesProved

  • The universal constant is a limit across dimensions

    Under stated assumptions

    If the sharp fixed-dimensional unit-slack constant is (n/(n+1))^n for every n ≥ 1, then the infimum of P(S < E S + 1) over all positive finite n and admissible distributions is 1/e. No fixed finite n attains this dimension-free infimum.

    Limit Finite-dimensional equality examples attain their own larger constants. The limiting value 1/e is approached as n grows, rather than attained in one finite dimension.

    Sources & review

    Source-grounded explanation · independent explanation review: pending.

Approaches

How the problem is attacked, and what each line of attack cannot yet reach.

An exact two-point extremizer

For δ ≥ 1, let each variable be 0 with probability 1−1/(n+δ), and n+δ otherwise. Each mean is one; the strict event occurs exactly when all variables are zero.

Cannot yet reach This construction shows sharpness in that parameter range. It does not establish optimality for 0 < δ < 1.

Sources & review

Supporting statements

Source-grounded explanation · independent explanation review: pending.

Timeline

  1. A broader Samuels proof is proposedProposal

    Ling’s later paper claims a formula for arbitrary mean vectors and all positive deviations.

    The general formula has its own assessment and is not covered by the unit-slack Lean theorem.

  2. Separately authored proofs of the unit-slack boundBound established

    Fu and coauthors and Nie–Wei post arguments reaching the sharp finite-n unit-slack constant.

    Authorship, AI contributions and mathematical input credits remain separate.

    Also on the Frontier: Feige's nonnegative-random-variable conjecture

  3. Feige’s probability questionFoundation

    The July papers cite Uriel Feige’s journal formulation of a lower-tail bound using independence and first moments.

    The conference version dates to 2004; this milestone uses the journal year.

  4. Unit-slack optimality has a public Lean proofFormalization

    Wang and Zhang’s project publishes the exact fixed-dimensional optimality declaration.

    The pinned source is inspected, without an OpenMath proof execution or an inferred first-publication date.

Full history with sources →

Evidence

Literature

3 preprints · 1 project

Status OpenMath assessment · Oct 13, 2026.

Formal

1 complete proof

1 formalization below ↓

Reported in sources: The pinned Lean source reports complete optimality for the unit-slack event. Deliberate unproved statement templates are separate from the solution imports. OpenMath has not built the project.

Computation

None recorded

Review

Not yet reviewed

OpenMath assessment: The unit-slack question is proved in two separately credited July papers, with finite-dimensional optimality reported complete in Lean. A later Samuels paper proposes the full sharp formula for arbitrary positive deviations.

Source comparison and reader curation; independent mathematical assessment remains pending.

OpenMath pilot collection · OpenMath source curation · assessed Oct 13, 2026 · review due Jan 13, 2027

Collection last checked Oct 13, 2026.

Formalizations

The optimal bound for a fixed number of variables →

Sharp finite-dimensional Feige inequalityComplete formal proof reported externally

Open formal source ↗

Complete formal proof reported externally

Lean 4 proof reports complete fixed-n optimality for δ = 1. It does not certify the July δ-dependent theorem or Ling’s Samuels proposal. Source definitions quantify over measurable, integrable, pointwise nonnegative independent variables on probability spaces.

Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026

Declaration & revision
PalomarFeige.sharp_unit_slack_feige_complete

Commit 19c61d6cb556d1e967dbb0ada9f293c290837867

External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.

Sources

Choose a starting point below. Each result links to its exact statement, cited passages and checks.

Start here

Bibliography 4

Research activity · 1 entry

Contributions

Fu, Han, Wang, Yan, Zhang and Zhou and Nie–Wei receive separate proof credits. The papers attribute different roles to GPT-5.6 Pro and GPT-5.6 Sol. Wang–Zhang’s Codex formalization is separately credited. Ling owns the later Samuels proposal; its source does not attribute a specific AI role.

Selected literature; source observations and coverage limits are retained in the publication details.

Record details
Record version
1
Classification
MSC2020 60E15 / 60G50
Prerequisite level
undergraduate
Source observations & version history →