我們很高興地宣佈推出 Trinity，這是我們在 @morph_labs 開發的用於驗證超級智慧的自動形式化系統。我們用它來在 Lean 中自動形式化 de Bruijn 的一個經典結果，即 abc 猜想幾乎總是正確的。

我們在這裡開源了 Trinity 對 de Bruijn 定理的完整形式化：