Chúng tôi rất vui mừng thông báo về Trinity, một hệ thống tự động hóa cho trí tuệ siêu việt đã được chúng tôi phát triển tại @morph_labs. Chúng tôi đã sử dụng nó để tự động hình thức hóa trong Lean một kết quả cổ điển của de Bruijn rằng giả thuyết abc là đúng gần như luôn luôn.

Chúng tôi đang mở mã hóa toàn bộ sự hình thức hóa của định lý de Bruijn của Trinity tại đây: