Lean4 membantu menemukan bug kecil dalam makalah terbaru Terence Tao

• Postingan Terence Tao di mathstodon.xyz
• Ditemukan bug kecil namun penting dalam makalah terbaru Terence Tao berkat proyek formalisasi Lean4
• Bug ditemukan saat proses formalisasi di halaman 6 makalah; makalahnya dapat dilihat di https://arxiv.org/pdf/2310.05328.pdf
• Dalam makalah Tao ditemukan ekspresi 12log⁡n−1n−k−1 yang menyimpang pada kasus n=3, k=2
• Masalah ini hanya muncul pada nilai n yang kecil, dan dapat diselesaikan dengan mengubah beberapa konstanta numerik pada halaman tersebut
• Untuk kasus n≥8, logikanya tetap valid, dan untuk n kecil kasusnya dapat ditangani dengan cara yang lebih sederhana
• Lean4 meminta Tao untuk membuktikan 0<n−3, tetapi ia hanya memiliki hipotesis n>2, sehingga muncul kontradiksi
• Tao berencana menambahkan catatan kaki yang mengakui adanya sedikit kesalahan yang ditemukan setelah mencoba formalisasi di Lean4 pada versi baru makalah tersebut
• Postingan ini memicu perhatian dan respons positif dari komunitas, sekaligus menekankan pentingnya alat bantu pembuktian dalam membangun fondasi yang kokoh untuk pekerjaan di masa depan

[GN⁺]

Komentar Hacker News

• Matematikawan terkenal Terence Tao menggunakan Lean4 dan GPT4 untuk menemukan bug kecil dalam makalah terbarunya.
• Proses Tao mempelajari Lean4 didokumentasikan dalam postingan Mastodon miliknya, sehingga menjadi studi kasus menarik tentang bagaimana Lean4 dapat mempercepat pekerjaan.
• Bagi pemula, Natural Number Game direkomendasikan sebagai pengenalan yang mudah ke Lean4.
• Seorang pengguna membagikan pengalamannya menggunakan TLA+ karya Lamport untuk membuat spesifikasi formal dan mengurangi kesalahan dalam pemrograman.
• Ada ketertarikan pada dependent types, meskipun implementasinya di compiler memiliki kompleksitas tersendiri.
• Kombinasi Lean4 dan automated theorem proving tampak sebagai perpaduan teknologi yang menjanjikan di masa depan, dengan potensi mendorong penemuan baru.
• Tao yang menggunakan Copilot untuk mempelajari Lean disorot sebagai contoh bagaimana Lean4 dapat mengurangi hambatan dalam mengadopsi alat baru.
• Perkembangan Tao dengan Lean4 dapat dilihat di GitHub miliknya.
• Seorang pengguna mengusulkan ide untuk menggabungkan formal proof checker dan language model guna menghasilkan pasangan dugaan-pembuktian sintetis, yang berpotensi berkembang menjadi kemampuan supermanusia dalam menghasilkan pembuktian.
• Istilah "bug" digunakan untuk menjelaskan kesalahan matematis, dan beberapa pengguna menganggapnya tidak biasa.