Probability · Conjecture
How small can be for a sum S of independent nonnegative random variables whose individual means are at most one?
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.
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.
Figures and explorable examples. Selecting a statement opens its exact wording.
The sharp constant for n variables, (n/(n+1))ⁿ, falls towards 1/e as n grows; earlier universal lower bounds sit well below it.
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.
Visual setup
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.
The atom at the threshold does not count: P(S < 4) adds only the mass at 0.
The conventional unit-slack conjecture. The stronger finite-n theorem yields this bound and approaches 1/e as n grows.
Bound · Primary formulation
ProvedFu et al. 2026The 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.
Both July arguments support the same mathematical assertion.
Theorem · Bound
ProvedFu et al. 2026The 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.
Fu–Han–Wang–Yan–Zhang–Zhou account
Sharp small-deviation inequalities
This account gives the sharp finite-dimensional unit-slack constant and a broader deviation inequality.
Its general deviation bound is sharp on the δ ≥ 1 branch; the later all-δ proposal is assessed separately.
Proved: Sharp unit-slack bound proved by Fu and coauthors ↗ · source dated Jul 27, 2026 · observed Oct 13, 2026. Theorem 1.1 at δ = 1, including finite-dimensional sharpness.
Nie–Wei account
A separate sharp-bound argument
A second author team establishes the same sharp finite-dimensional unit-slack constant.
The Wang–Zhang formal project has its own scope; credit for this mathematical argument remains separate.
Proved: Unit-slack bound proved by Nie and Wei ↗ · source dated Jul 27, 2026 · observed Oct 13, 2026. Their separately authored proof reaches the same finite-dimensional constant.
Independent mathematical assessment of an argument remains separate from the statement’s attributed status.
Ling’s later Corollary 1.3 proposes the fully sharp formula; it is not part of the linked unit-slack Lean proof.
Bound · Different statement · related variant
ProposedLing 2026The 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.
Finite-dimensional equality examples attain their own larger constants.
Theorem · Conditional implication
ProvedFu et al. 2026The universal constant is a limit across dimensions
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.
An earlier universal lower bound, superseded by the sharp constant 1/e.
Bound · Related result
ProvedFeige 2004 · per Fu et al. 2026Feige’s first universal lower bound: 1/13
An earlier lower bound on the unit-slack probability, before the sharp 1/e.
An earlier universal lower bound, superseded by the sharp constant 1/e.
An earlier universal lower bound, superseded by the sharp constant 1/e.
Bound · Related result
ProvedHe, Zhang & Zhang 2010 · per Fu et al. 2026A fourth-moment lower bound: 1/8
An earlier lower bound on the unit-slack probability, before the sharp 1/e.
An earlier universal lower bound, superseded by the sharp constant 1/e.
An earlier universal lower bound, superseded by the sharp constant 1/e.
Bound · Related result
ProvedGuo, He, Ling & Liu 2020 · per Fu et al. 2026A moment and Berry–Esseen lower bound: 0.1798
An earlier lower bound on the unit-slack probability, before the sharp 1/e.
An earlier universal lower bound, superseded by the sharp constant 1/e.
The first branch is a lower bound, without a sharpness claim.
Bound · Different statement · related variant
ProvedFu et al. 2026The July bounds in two deviation ranges
The first branch is a lower bound, without a sharpness claim. Nie–Wei prove the first expression for unit means and 0 < δ ≤ 1; shifting each variable by 1 minus its mean extends that statement to means at most one.
This attains the fixed-n bound. The dimension-free constant 1/e is approached as n grows and is not attained by this family at finite n.
The optimal bound for a fixed number of variables →Sharp finite-dimensional bound related to Dimension-free unit-slack bound.
Scope comparisonFinite-dimensional and universal bounds. The finite constants (n/(n+1))^n decrease to 1/e; each is strictly larger than 1/e.
Limit Finite-n sharpness and the limiting universal bound are not identical statements.
Independent relationship review: not recorded. Link to this connection
Assuming Sharp finite-dimensional boundProved
The universal constant is a limit across dimensions
Under stated assumptionsIf 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.
Source-grounded explanation · independent explanation review: pending.
How the problem is attacked, and what each line of attack cannot yet reach.
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.
Supporting statements
Source-grounded explanation · independent explanation review: pending.
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.
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.
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.
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.
| Literature | Status OpenMath assessment · Oct 13, 2026.
|
|---|---|
| Formal | 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 | |
| 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. |
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
PalomarFeige.sharp_unit_slack_feige_completeCommit 19c61d6cb556d1e967dbb0ada9f293c290837867
External proof reports do not establish an OpenMath run, independent statement correspondence, or independent mathematical review.
Choose a starting point below. Each result links to its exact statement, cited passages and checks.
Read the mathematical argument; inspect its statement for assessment and scope.
Read the mathematical argument; inspect its statement for assessment and scope.
Inspect the formal statement, assumptions and reported checks.
Weibo Fu · Yanjun Han · Guanyang Wang · Jun Yan · Peng Zhang · Zhengqing Zhou · Preprint · Jul 27, 2026
Theorem 1.1, Corollary 1.2 and AI disclosure
Zipei Nie · Jiaye Wei · Preprint · Jul 27, 2026
Theorem 1.3 and AI acknowledgement; arXiv submitted 27 July, HTML manuscript dated 24 August
Zhi Ling · Preprint · Aug 18, 2026
Theorem 1.1 and Corollary 1.3; arXiv submitted 18 August, manuscript dated 19 August
Guanyang Wang · Peng Zhang · Project documentation
PalomarFeige.sharp_unit_slack_feige_complete; README and formalization metadata
Research direction
Compare Ling’s reduction and weighted Bernoulli argument with the July bounds and the exact Samuels statement.
No independent assessment or formal proof of this later proposal is recorded.
Related statements · context, not additional proved progress
Selected literature; source observations and coverage limits are retained in the publication details.
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.
Weibo Fu · Yanjun Han · Guanyang Wang · Jun Yan · Peng Zhang · Zhengqing Zhou
The authors report GPT-5.6 Pro assistance in proof discovery; the calibration theorem of Vlassis and Thomas and Grünbaum-type inequalities are mathematical inputs, not authors of this paper.
Zipei Nie · Jiaye Wei
Nie and Wei credit GPT-5.6 Sol for exploration and discovery, state that they checked the arguments and authored the text, and retain responsibility. Their argument uses the Vlassis–Thomas calibration theorem.
Zhi Ling
No specific AI contribution is attributed by this source record.
Guanyang Wang · Peng Zhang
The project credits GPT-5.6 Sol Codex for formalization. This is a different contribution from the July discovery model. Authors report verification; OpenMath has not executed it.
These are source credits; they do not imply OpenMath accounts, endorsements or independent mathematical review.