Vi är glada över att kunna presentera Trinity, ett autoformaliseringssystem för verifierad superintelligens som vi har utvecklat vid @morph_labs. Vi har använt det för att automatiskt formalisera i Lean ett klassiskt resultat av de Bruijn att abc-förmodan nästan alltid är sann.

Vi använder öppen källkod för Trinitys fullständiga formalisering av de Bruijns sats här: