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

Мы открываем исходный код полной формализации теоремы де Бруйна Trinity здесь: