Temos o prazer de anunciar o Trinity, um sistema de autoformalização para superinteligência verificada que desenvolvemos na @morph_labs. Nós o usamos para formalizar automaticamente em Lean um resultado clássico de de Bruijn de que a conjectura abc é verdadeira quase sempre.

Estamos abrindo o código da formalização completa do Trinity do teorema de Bruijn aqui: