用 616,873 行 Lean 证明 1 + 1 = 2

一份 Lean 4 形式化证明用 616,873 行代码证明了 1 + 1 = 2，包含 101,708 个定理和 100,714 个定义，不依赖 Mathlib，也不使用 Lean 内置的自然数、整数或有理数。