**零公理 Lean 4 证明：四维欧氏空间上的杨 - 米尔斯理论是“圆方”**

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

> 该资讯展示了一个基于 Lean 4 的形式化数学证明，该证明在零公理（Zero Axiom）框架下，论证了在四维欧氏空间 R^4 上定义的杨 - 米尔斯理论（Yang-Mills）具有“圆方”（Round Square）这一几何性质，即同时具备圆的性质和正方形的性质。

**来源信息**
- **来源**：Hacker News：AI 热帖
- **分类**：论文
- **发布时间**：2026-11-05 05:20（北京时间）
- **原文**：[打开原文](https://zenodo.org/records/23918639/files/RoundSquare.lean?download=1)