Estamos entusiasmados em anunciar o Trinity, um sistema de autoformalização para superinteligência verificada que desenvolvemos na @morph_labs. Usamos isso para formalizar automaticamente em Lean um resultado clássico de de Bruijn que a conjectura abc é verdadeira quase sempre.

Estamos a disponibilizar como código aberto a formalização completa do teorema de de Bruijn do Trinity aqui: