Kami dengan senang hati mengumumkan Trinity, sistem autoformalisasi untuk kecerdasan super terverifikasi yang telah kami kembangkan di @morph_labs. Kami telah menggunakannya untuk secara otomatis memformalkan dalam Lean hasil klasik de Bruijn bahwa dugaan abc hampir selalu benar.

Kami membuka sumber formalisasi lengkap Trinity tentang teorema de Bruijn di sini: