第三方复核:零公理 Lean 4 形式化成立,但并未真正解决千禧年 Yang–Mills 难题

kevrussell · x · 2026-11-06

honesty.tools 团队对 RoundSquare 宣称的「世界首个零公理 Lean 4 形式化证明、负向解决 Clay Yang–Mills 千禧年难题」进行了独立核查。

成立的部分:

不成立的部分:

该形式化与 Clay 官方 Yang–Mills 陈述并不对齐:无规范群 G、用的是 ℝ⁴ 上的 flag 而非 QFT、只覆盖五维 flag 情形、仅有经典相对 no-go

结论:内核认证的是「证明本身」,而不是其宣称的「解决千禧年难题」这一标题。值得注意的是 advertised 74 条定理、实际只有 114 个审计点,CI 并不保证 COUNT==74。

「Fun」频道最新