Feige’s small-deviation conjecture

Feige's conjecture for slack at least 1

Model / AI: GPT-5.6 Pro

ChatGPT 5.6 Pro found the proof of the sharp bound for every δ >= 1, connecting the 18-day-old Dirichlet calibration theorem of Vlassis and Thomas to Grünbaum's centroid inequality and its Letwin-Yaskin generalization; the sorry-free Lean formalization covers the unit-slack case δ = 1 only, and δ < 1 stays open. Peer review pending.

Source read 2026-09-08. Read the arXiv abstract: the authors credit ChatGPT 5.6 Pro and state sharpness for δ ≥ 1. Lean coverage was not audited.

• Paper — Feige's conjecture for slack at least 1
• Lean — Lean formalization