我们很高兴地宣布Trinity，这是我们在@morph_labs开发的一个用于验证超智能的自动形式化系统。我们已经使用它在Lean中自动形式化了de Bruijn的一个经典结果，即abc猜想几乎总是正确的。

我们在这里开源了Trinity对de Bruijn定理的完整形式化：