Lean 形式化证明了 Feige 猜想的 $\delta\ge 1$ 情形
RexDouglass · x · 2026-07-28
一篇新的 arXiv 论文给出独立非负随机变量和的尖锐小偏差不等式，并在 $\delta\ge 1$ 的情形下证明了 Feige 猜想。
论文结论
- 对独立非负随机变量 $Xi$ 且 $\mathbb{E}Xi\le 1$，作者给出
$\mathbb{P}(S<\mathbb{E}S+\delta)$ 的显式下界 $b{n,\delta}$。
- 当 $\delta\ge 1$ 时，这个界是锐的，并且满足 $b{n,\delta}\ge e^{-1}$，因此得到 Feige 猜想在该区间上的正解。
证明思路
- 证明组合了 Vlassis 和 Thomas 最近关于 Gaffke 猜想 的统计学结果。
- 还用到了凸几何中的 Grünbaum 中心超平面定理，以及 Letwin 和 Yaskin 的推广。
- 作者还把整套证明形式化到了 Lean。
帖主补充说，GPT-5.6 参与生成了证明草图。
「研究」频道最新
- Reddit 用户用 LoRA 和 ComfyUI 做出 Wan 2.2 连续生成流程 — SnooMacaroons1365 · 2026-07-28
- Kimi K3 复现 RLVR 研究结论且不乱下结论 — infoxiao · 2026-07-28
- 中科院论文梳理基础模型长程规划的形成与蒸馏机制 — CASIA · 2026-07-28
- 首个机器人三视角世界模型榜单 TriWorldBench 发布 — 机器之心 · 2026-07-28
- 120 张标注图训练出一个 5MB 的 McBess 风格 LoRA — Winter_unmuted · 2026-07-28
- GaussianGPT 用自回归 next-token 生成 3D Gaussian 场景 — rsasaki0109 · 2026-07-28