Ми раді оголосити про Trinity, систему автоформалізації для перевіреного суперінтелекту, яку ми розробили в @morph_labs. Ми використали його для автоматичної формалізації в Lean класичного результату де Брюйна, що гіпотеза abc вірна майже завжди.

Повну формалізацію теореми де Брюйна ми наводимо тут: