Hodge 与 Yang-Mills 猜想尚无完整 Lean 形式化，短期更难被攻克
Jsevillamol · x · 2026-09-23
作者 Jsevillamol 指出一个容易被忽视的事实：Hodge 猜想和 Yang-Mills 存在性与质量间隙这两个千禧年大奖难题，目前还没有完整形式化的 Lean 陈述。
在他看来，没有可机器验证的形式化命题，会显著降低这些问题近期被（尤其是被 AI 辅助）解决的概率，不过他对长期前景仍然乐观。他此前曾提出以「附带 Lean 证明凭证」作为判定问题解决的严格标准，并指出目前五个问题中已有约 3/5 被接受 Lean 形式化，其余缺口有望逐步补齐。
「研究」频道最新
- Quanta 解读：定价算法无需合谋也能推高物价 — burny_tech · 2026-09-23
- CodeMidas：从源码自动生成可执行的编码 RL 训练环境 — burny_tech · 2026-09-23
- 学者怀念 20 年前的方法论论文:没有防御性废话直击要点 — PMinervini · 2026-09-23
- 新论文：块三角联合漂移实现单步生成式代理模型 — chaumian · 2026-09-23
- LLM 当概率分类器不够,研究者提醒需校准才能用于决策 — PMinervini · 2026-09-23
- 自我纠错:并行搜索削弱 Grover 优势,AES-256 更难被量子破解 — Jsevillamol · 2026-09-23