我真的很担心这周有多少数学家告诉我“如果它在 Lean 中编译通过，我们就知道它是真的”。Lean 很棒，但这实在是危险的错误。 以下是 50 种在 Lean 中证明 1 == 0 的方法。这些方法可以编译。具体取决于你使用的版本。 （链接在评论中）