我真的很擔心這周有多少數學家告訴我「如果在 Lean 中編譯成功，我們就知道這是真的」。Lean 很棒，但這是危險的錯誤。 這裡有 50 種方法可以在 Lean 中證明 1 == 0。這些都能編譯。根據你使用的版本而定。 （鏈接在評論中）