We zijn enthousiast om Trinity aan te kondigen, een autoformalisatiesysteem voor geverifieerde superintelligentie dat we hebben ontwikkeld bij @morph_labs. We hebben het gebruikt om automatisch een klassiek resultaat van de Bruijn in Lean te formaliseren, namelijk dat de abc-conjectuur bijna altijd waar is.

We maken de volledige formalisering van de Bruijn's stelling van Trinity hier open source: