Hacker News · Show HN 项目发现· DRLogvinovich·2026-11-05 05:20· 3 小时前

Show HN：零公理 Lean 4 证明 R^4 上 Yang-Mills 是“圆方”

Show HN: Zero-axiom Lean 4 proof that Yang-Mills on R^4 is a "round square"

AI 导读

开发者发布 2,576 行自包含 Lean 4 脚本 RoundSquare.lean，形式化证明在非紧 R^4 上同时要求完整 Osterwalder-Schrader/Wightman 公理与严格谱隙 Δ > 0 存在结构性矛盾。