Z radością ogłaszamy Trinity, system automatycznej formalizacji dla zweryfikowanej superinteligencji, który opracowaliśmy w @morph_labs. Użyliśmy go do automatycznej formalizacji w Lean klasycznego wyniku de Bruijna, że hipoteza abc jest prawdziwa prawie zawsze.

Udostępniamy tutaj pełną formalizację twierdzenia de Brujna przez Trinity jako open source: