Vi er glade for å kunngjøre Trinity, et autoformaliseringssystem for verifisert superintelligens som vi har utviklet i @morph_labs. Vi har brukt det til å automatisk formalisere i Lean et klassisk resultat av de Bruijn at abc-formodningen er sann nesten alltid.

Vi åpner Trinitys fullstendige formalisering av de Bruijns teorem her: