Matematikawan manusia tersalip AI dalam menemukan kontracontoh

• Model keluarga ChatGPT dan Claude hanya dalam beberapa minggu telah membuat kontracontoh untuk dugaan jarak satuan Erdős, pertanyaan skema grup Grothendieck, dan Jacobian Conjecture, dan sebagian telah diverifikasi dengan Lean
• Sol dari OpenAI memformalkan kontracontoh Erdős beserta hasil teori medan kelas global yang diperlukan dalam 3 minggu dengan 1,2 juta baris kode Lean, skala yang lebih dari setengah 2,3 juta baris mathlib yang ditulis selama 9 tahun
• Untuk pertanyaan Grothendieck yang sudah berusia 60 tahun, Sol menemukan kontracontoh 12 halaman dan Fable memformalkannya menjadi 1.076 baris dalam 4 jam, mengonfirmasi keberadaan skema grup berorde 4 tetapi tidak dimatikan oleh 4
• Formasilasi otomatis juga sangat meningkatkan kecepatan riset, dengan Andrew Yang menulis 250 ribu baris kode Lean selama sekitar 2 minggu dan pada praktiknya menyelesaikan proyek teorema modularity lifting yang dibutuhkan untuk Teorema Terakhir Fermat
• Matematika informal yang dihasilkan AI tidak bisa langsung dipercaya, tetapi jika dugaan diubah menjadi pernyataan Lean yang tepat maka pembuktian dan sanggahannya bisa diperiksa secara mekanis, dan manusia harus menarik wawasan matematis yang lebih dalam dari kontracontoh tersebut

---

Dugaan jarak satuan Erdős dan teori medan kelas global

• Pada 20 Mei 2026, ChatGPT membantah dugaan jarak satuan Erdős di geometri diskret
  • Kontracontoh dibangun menggunakan teorema bilangan yang mendalam dari Golod dan Shafarevich pada 1960-an
  • Sejumlah matematikawan meninjau argumen itu sebelumnya dan menilainya valid, tetapi saat diumumkan belum ada formalisasi Lean
• Pada 26 Mei, peraih Fields Medal sekaligus kepala ilmuwan Logical Intelligence Mike Freedman mengumumkan bahwa sistem perusahaannya telah secara otomatis memformalkan seluruh makalah ChatGPT ke Lean
  • Cakupan formalisasi adalah pernyataan bahwa teorema Golod–Shafarevich mengimplikasikan kontracontoh Erdős
  • Teorema bilangan dasarnya sendiri membutuhkan lebih dari 100 halaman dan bergantung pada bagian besar dari teori medan kelas global
• Selama setahun setelah sekolah musim panas formalisasi teori medan kelas 2025, kasus lokal hampir selesai, tetapi kasus global masih belum terpecahkan

Formalisasi lengkap 1,2 juta baris buatan Sol

• Pada 26 Juni, Boris Alexeev dari OpenAI mengungkapkan di Lean Zulip bahwa ia telah mengarahkan model baru Sol untuk membuat formalisasi lengkap kontracontoh Erdős yang tidak mengasumsikan apa pun selain aksioma matematika
• Selama 3 minggu, Sol menghasilkan 1,2 juta baris kode Lean
  • mathlib yang ditulis selama 9 tahun berjumlah 2,3 juta baris
  • Kualitas kodenya tidak merata, tetapi benar-benar membuktikan hasil sulit dalam teori medan kelas global dan teorema nontrivial tentang kohomologi medan bilangan
• Karena Lean adalah bahasa pemrograman yang bisa menjalankan perintah arbitrer, kode hasil generasi dijalankan dalam sandbox dengan mempertimbangkan kemungkinan adanya kode berbahaya
• Skala dan kecepatan ini mengarah pada penilaian bahwa pengembangan matematika yang dihasilkan AI dalam skala besar tak terelakkan

Workshop Formalizing Fermat dan aksesibilitas alat

• Workshop Formalizing Fermat pada 6–10 Juli dihadiri 25 orang, tetapi sistem formalisasi otomatis dari sponsor Logos Research hanya bisa dipakai 5 orang secara bersamaan
• Semua peserta diberi langganan Claude Max selama sebulan agar bisa memakai Claude Fable, dan OpenAI juga memberi akses ChatGPT Pro gratis selama sebulan
  • Sol dijadwalkan rilis pada 9 Juli
  • Fable dijadwalkan berakhir pada 7 Juli tetapi akses nyatanya tetap dipertahankan
  • Peserta bisa memakai Sol dan Fable selama 4 dari 5 hari workshop, dan alat Logos selama keseluruhan acara
• Untuk mengembangkan teori skema grup datar hingga yang dibutuhkan dalam formalisasi Teorema Terakhir Fermat, makalah klasik dimasukkan ke Fable dan ChatGPT untuk menghasilkan penjelasan bahasa alami
  • Logos menemukan bahwa satu proposisi di dalam penjelasan itu salah dan mengajukan kontracontoh eksplisit
  • Setelah diperiksa, dokumen buatan LLM yang menjelaskan konstruksi standar itu memang keliru, dan manusia melewatkan kesalahannya saat membaca
  • Perbedaannya adalah sistem ini tidak sekadar menjawab bahwa ia tidak memahami argumen itu, tetapi memberikan bukti bahwa argumen itu salah

Pertanyaan Grothendieck tentang skema grup

• Profesor UChicago Akhil Mathew mengajukan kepada AI pertanyaan lama Grothendieck: apakah setiap skema grup bebas hingga berorde (n) dimatikan oleh (n)
  • Deligne membuktikan kasus komutatif
  • Grothendieck membuktikan kasus ketika ruang dasarnya reduced
  • Rene Schoof menangani lebih banyak kasus, dan Emiliano Torti juga membuktikan kasus yang lebih umum dalam makalah tahun sebelumnya
• Pada 11 Juli, sehari setelah workshop, Sol menemukan kontracontoh dan menghasilkan PDF 12 halaman
  • Ketika diminta bukan hasil informal melainkan formalisasi Lean penuh, Fable memformalkannya secara otomatis menjadi 1.076 baris dalam 4 jam
• Berkas Lean itu lebih dulu diperiksa untuk memastikan isinya hanya teorema tanpa perintah seperti penghapusan file, lalu dikompilasi di laptop
  • Diperiksa apakah pernyataannya hanya memakai konsep dari mathlib
  • Diperiksa apakah pernyataannya benar-benar menyatakan keberadaan kontracontoh
  • Diperiksa apakah buktinya berhasil dikompilasi dengan benar
  • Seluruh verifikasi memakan waktu kurang dari 5 menit
• Hasil verifikasi menunjukkan bahwa ada skema grup berorde 4 tetapi tidak dimatikan oleh 4
• Akhil Mathew mengajukan kontracontoh ini sebagai mathlib PR
• Kontracontoh Erdős berukuran sekitar 1 juta baris, sedangkan kontracontoh Grothendieck hanya sekitar 1.000 baris dan jauh lebih sederhana, tetapi ini menjadi contoh mesin memecahkan pertanyaan aljabar geometri yang telah berusia 60 tahun

Reaksi para ahli dan teorema modularity lifting

• Pada 14 Juli, seorang profesor di Imperial College menilai bahwa fakta kontracontoh Grothendieck mudah ditemukan hanya menunjukkan bahwa manusia belum cukup lama memikirkan masalah itu
• Mahasiswa doktoral Andrew Yang memakai Sol dan Fable saat memformalkan teorema modularity lifting yang penting untuk Teorema Terakhir Fermat dalam Lean
  • Ia menulis sekitar 250 ribu baris kode Lean selama kurang lebih 2 minggu
  • Dengan itu, proyek tersebut pada praktiknya selesai
• Profesor lain di Imperial awalnya sulit memahami mahasiswa pascasarjana membayar 200 dolar per bulan untuk Sol dan Fable, tetapi setelah melihat hasil ini justru menilai bahwa mahasiswa doktoral yang tidak mengeluarkan 200 dolar per bulan untuk alat tersebut bersikap tidak rasional
• Harvard sudah memberikan akses gratis ke Fable kepada semua mahasiswa doktoral, postdoc, dan profesor

Kontracontoh Jacobian Conjecture

• Akhil Mathew dan Levent Alpöge mendiskusikan cara mencari kontracontoh tambahan di aljabar geometri, dan Fable menemukan kontracontoh untuk Jacobian Conjecture, masalah terkenal yang terbuka selama sekitar 100 tahun
• Levent Alpöge mengungkapkan di X hasil yang tampaknya terselesaikan saat final Piala Dunia 2026
• Ketika Akhil Mathew mengusulkan mathlib PR baru, Paul Lezeau ternyata sudah lebih dulu memformalkan kontracontoh itu secara manual dan mengajukan PR ke repositori Formal Conjectures milik DeepMind
• mathlib tidak memiliki daftar besar dugaan matematika, tetapi repositori Formal Conjectures memilikinya
• Jika manusia menyepakati pernyataan Lean yang secara setia menangkap makna dugaan tersebut, maka pekerjaan memeriksa apakah kode buatan AI membuktikan atau menyangkal dugaan itu menjadi sederhana

Tugas yang tersisa bagi manusia setelah verifikasi formal

• Untuk Jacobian Conjecture, langkah berikutnya bagi manusia adalah memahami apa tepatnya yang terjadi di dalam kontracontoh itu
• Untuk kontracontoh Grothendieck juga sedang berlangsung upaya memahami lebih dalam, melampaui sekadar mendaftarkan representasi ring arbitrer dan perhitungannya
• Nilai kontracontoh tidak berhenti pada penutupan masalah secara formal; nilainya menjadi lengkap dalam proses mengekstrak wawasan agar manusia bisa memahami matematika dengan lebih baik

[GN⁺]

Komentar di Lobste.rs

• Ini benar-benar hasil yang mengejutkan. Ini adalah dugaan yang terkenal dan mudah didekati, sampai-sampai tahun lalu dosen kalkulus multivariabel saya memberikannya sebagai soal bonus seperti lelucon
  Jika akrab dengan geometri aljabar, secara retrospektif terlihat jalur yang cukup alami untuk membangun contoh tandingan, dan LLM juga bisa menyajikan intuisi seperti ini, jadi ini bukan contoh tandingan yang muncul begitu saja. Selain itu, jika dilihat kembali, ada petunjuk yang mengisyaratkan bahwa dugaan itu salah, dan sebelumnya juga sudah ada contoh tandingan buatan manusia untuk versi dugaan yang dimodifikasi
  Contoh tandingan kali ini adalah fungsi tiga variabel C^3 → C^3, dan dugaan 2 dimensi masih belum terpecahkan. Ada juga hasil yang menunjukkan bahwa jika contoh tandingan 2 dimensi ada, ia harus jauh lebih rumit dibanding yang ini
  Meski begitu, ini tetap pencapaian besar karena merupakan dugaan terkenal yang telah lama diteliti para matematikawan. Berbeda dengan dugaan jarak satuan, pandangan para pakar tentang benar-tidaknya dugaan ini juga terbelah, jadi bukannya selama ini tidak ada orang yang mencoba mencari contoh tandingan. Ini bukan hasil yang bisa ditemukan dengan brute force, dan jelas modelnya tidak sekadar mencacah contoh tandingan secara membabi buta

• Eksplorasi program yang dipandu LLM terasa seperti arah ke depan. Memformalkan satu kernel saja sudah luar biasa, tetapi kini rasanya kita jauh lebih dekat dengan impian untuk menyatakan properti kebenaran formal suatu modul dan menurunkan implementasi yang terbukti benar
  Masih dibutuhkan banyak kreativitas manusia untuk memilih teorema mana yang akan diformalkan dan menentukan cara mengarahkan implementasi agar praktis, dan kemungkinan itu sangat menarik

• Dugaan Jacobian jelas cukup layak masuk 100 besar masalah terbuka matematika, sedangkan dugaan jarak satuan oleh GPT mungkin sekitar 1.000 besar. Pada akhir abad ke-20, beberapa daftar diajukan sebagai penerus masalah Hilbert, dan Millennium Prize Problems adalah yang paling luas diakui, tetapi masalah Smale juga mendekati status itu, dan dugaan Jacobian termasuk di dalamnya
  Namun, karena kasus 2 dimensi masih terbuka, kurang tepat mengatakan bahwa AI telah memecahkan salah satu masalah Smale, versi abad ke-20 dari masalah Hilbert. Dugaan Poincaré juga sudah dibuktikan untuk dimensi 5 ke atas pada 1961 dan dimensi 4 pada 1982, tetapi inti masalahnya, dimensi 3, baru diselesaikan pada 2003
  Banyak matematikawan berpandangan bahwa dugaan Jacobian salah untuk dimensi 3 ke atas, dan ini bukan rasionalisasi setelah kejadian. Tulisan Peter Woit tahun 2004, yang menunjukkan sudut pandang matematikawan di luar bidang spesialisnya, juga menulis bahwa “dugaan Jacobian adalah salah satu masalah terbuka paling terkenal dalam geometri aljabar, dan Carolyn Dean tampaknya telah membuktikannya untuk polinomial dengan dua variabel kompleks. Jika variabelnya lebih banyak, banyak orang percaya dugaan itu tidak benar”

• Saya bukan matematikawan, tetapi sepertinya pencarian kerentanan dan pencarian contoh tandingan punya area yang tumpang tindih. Keduanya adalah proses mencari cara agar sistem kompleks berperilaku salah

  • Itu intuisi yang tepat. Saat melakukan verifikasi formal dengan solver SMT, kita memasukkan prasyarat dan pascasyarat di sekitar kode yang akan diperiksa, dan ini disebut triple Hoare (Hoare triple). Jika solver SMT menemukan input yang tidak memenuhi kondisi, itu secara harfiah disebut contoh tandingan
    Saat bekerja di perusahaan verifikasi formal pun, kami menyebut hasil eksplorasi sebagai contoh tandingan, bukan bug atau kerentanan. Karena hasilnya bergantung pada spesifikasi, istilah ini lebih tepat. Bahkan untuk masalah kebenaran pada bahasa atau compiler, sulit menilai apakah sesuatu benar-benar bug atau fitur yang disengaja tanpa spesifikasi
  • Ini juga alasan mengapa sebagian besar pengujian adalah pemeriksaan empiris. Seperti penelitian empiris, prosesnya bukan membuktikan proposisi, melainkan mencari contoh tandingan

• Jika kode Lean berbahaya bisa menjalankan perintah arbitrer, saya ingin kembali ke masa lalu dan membuat ulang Lean agar tidak bisa menjalankan perintah arbitrer. Untuk penggunaan sah ketika bahasa pembukti teorema perlu menjalankan skrip shell, berikan superset atau izin tambahan, lalu sebut bahasa itu Bloated

  • Lean punya monad dan tampaknya semestinya pada dasarnya merupakan bahasa fungsional murni. Jadi rasanya cukup memeriksa bahwa tipe teorema utama tidak setara dengan IO milik Lean, serta memeriksa apakah fitur yang setara dengan unsafePerformIO digunakan. Namun, saya tidak tahu apakah ada jalan keluar mencurigakan lainnya
  • Akan bagus jika memperkenalkan struktur seperti unsafe di Rust, lalu mensyaratkan argumen tambahan seperti --unsafe-allow-unsafe untuk mengizinkan sintaks berbahaya. Banyak bahasa khusus domain (DSL) juga bisa mendapat manfaat jika bahasanya dipisahkan seperti ini

[GN⁺]

Komentar Hacker News

• Saat di pascasarjana, saya pernah mendapat kesempatan berkontribusi langsung pada sebuah masalah terbuka dalam kelas riset dosen pembimbing saya. Pada suatu Jumat, sang profesor mengajukan sebuah dugaan yang mulus dan indah yang ia harapkan benar, tetapi saya, yang menyukai pengecualian aneh dan juga kekurangan alat pembuktian, berfokus mencari contoh tandingan dan menemukannya dalam satu jam.
  Profesor itu gagal membuktikannya sepanjang akhir pekan, dan kejadian itu menunjukkan bahwa ketika orang-orang dengan alat, ekspektasi, dan motivasi berbeda melihat masalah yang sama, mereka bisa berkontribusi dari arah yang sama sekali berbeda. Saya tentu tidak bisa dibandingkan dengan pembimbing hebat itu, tetapi saat itu saya punya alasan untuk melihat ke arah lain, dan itu berujung pada contoh tandingan kecil yang menjadi satu-satunya kontribusi riset matematika saya.

  • Sepertinya ini juga alasan mesin pandai menemukan contoh tandingan. Mereka tidak punya keterikatan estetis pada sebuah dugaan, dan tidak merasa malu mengeluarkan hasil yang jelek.
  • Sebagai matematikawan, perasaan saya justru sebaliknya. Pembuktian bisa dilakukan dengan sedikit memodifikasi bukti yang sudah diketahui, tetapi untuk membuat contoh tandingan kita perlu memahami struktur objeknya secara mendalam, sehingga sering kali melampaui kemampuan saya.
    Namun, ini mungkin karena saya terutama menangani objek abstrak yang sulit saya pahami; untuk bilangan atau polinomial, kemungkinan besar kebalikannya.
  • Profesor, peneliti, dan guru yang membuka masalah yang belum terpecahkan kepada mahasiswa dan mengajak mereka berpartisipasi seharusnya lebih dihargai. Dalam kelas teknik pertama saya di universitas, ketika dosen berkata kepada mahasiswa tahun pertama, “Ini masalah-masalah yang belum bisa kita selesaikan, jadi beri tahu saya kalau kalian punya ide,” saya merasa lebih diterima dan menjadi bagian dari komunitas dibanding sebelumnya, dan itu sangat menginspirasi di awal masa studi yang bisa saja terasa membosankan.
  • Ada cerita yang nyaris sama dalam 《How to Solve It》.
  • Ada anekdot Zeeman yang lebih ekstrem dan arahnya berlawanan. Ia menghabiskan bertahun-tahun mencoba menemukan bola yang tersimpul di ruang 5 dimensi, lalu menyadari bahwa itu mustahil dan membuktikannya hanya dalam beberapa jam.
    https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...

• Yitang Zhang, yang terkenal karena dugaan bilangan prima kembar, meneliti dugaan Jacobian selama 7 tahun di Purdue di bawah bimbingan Tzuong-Tsieng Moh. Ternyata langkah kunci dalam disertasinya bergantung pada korolari Moh yang keliru; Moh menolak menulis surat rekomendasi, dan Zhang tidak bisa mendapatkan posisi pengajaran atau riset sehingga harus bekerja selama bertahun-tahun di Subway.
  Saya penasaran apa yang akan terjadi seandainya ChatGPT sudah ada saat ia memulai riset pada 1986. Sekarang kisah itu menjadi cerita sukses yang mengharukan, tetapi seperti bait puisi “Yu Xin menjalani hidup yang amat sunyi, namun puisi dan fu pada masa tuanya mengguncang wilayah sungai dan perbatasan,” kisah ini membangkitkan perasaan yang rumit.

  • Pernah ada dosen penguji yang menemukan cacat dalam pembuktian saat presentasi doktor matematika. Setelah si mahasiswa memahaminya lalu bertanya, “Sekarang saya harus bagaimana?”, dosen penguji itu hanya mengangkat bahu.
  • Karena kemudian ia berhasil pada dugaan bilangan prima kembar, kisah itu memang bisa disebut mengharukan, tetapi saya lelah dengan cerita-cerita seperti ini di dunia akademik. Terlalu banyak politik dan pengelolaan reputasi, dan Zhang seharusnya tidak perlu mengalami penderitaan seperti itu.
    Saat memperluas riset saya ke matematika, saya terkejut melihat banyak proposisi dalam literatur ternyata salah dan telah menyebar luas hingga ke literatur terapan. Bahkan ketika masalahnya diberitahukan, responsnya sering berupa defensif dan penyangkalan, seperti dalam kisah Zhang. LLM berguna untuk pembuktian, tetapi juga bisa sangat keliru; ia mirip satu orang lagi yang menawarkan arah eksplorasi dengan intuisi berbeda, jadi saya kira hasilnya akan tetap sama pada 1986.
  • Arti puisi yang diterjemahkan ChatGPT kira-kira adalah “Hidup Yu Xin sepenuhnya muram, tetapi puisi dan fu pada masa tuanya mengguncang Jiangguan.”

• Dalam matematika, contoh tandingan sangat penting untuk memperhalus definisi dan mempertajam pembuktian. Saya merekomendasikan buku Imre Lakatos tahun 1976, 《Proofs and Refutations》; ada juga cukup banyak buku di topologi, teori probabilitas, analisis, dan bidang lain yang hanya membahas contoh tandingan.
  https://en.wikipedia.org/wiki/Proofs_and_Refutations
  https://www.amazon.com/s?k=counterexamples

• Jika kita menemukan contoh tandingan, kita tidak membuang waktu membuktikan proposisi yang salah dan bisa beralih ke masalah lain; setidaknya dalam matematika, itu membuat waktu umat manusia digunakan lebih produktif.

  • Pembantahan lewat contoh tandingan memang efektif, tetapi pada akhirnya kurang memuaskan. Ia memberi jawaban, tetapi tidak membuat kita memahami mengapa matematika bekerja seperti itu atau menuntun ke pertanyaan baru.
    Selama manusia masih menilai apa yang merupakan pembuktian yang elegan dan penuh wawasan, pekerjaan matematikawan manusia masih akan ada.
  • Contoh tandingan juga berguna untuk memperbaiki pernyataan sebuah teorema. Dalam riset ilmu komputer teoretis, lazim terjadi proses mencoba membuktikan teorema yang kita harapkan benar, menemukan contoh tandingan, lalu memodifikasi pernyataannya dan melanjutkan.
    Fakta bahwa banyak teorema ilmu komputer berurusan dengan definisi induktif dan koinduktif juga membantu.
  • Terutama jika contoh tandingannya telah diverifikasi secara formal, upaya spekulatif bertahun-tahun bisa hampir seketika berubah menjadi jawaban yang pasti.
  • Namun secara keseluruhan, kita tidak bisa memastikan bahwa waktu digunakan lebih produktif. Baik membuktikan maupun membantah sebuah proposisi, dan terlepas dari apakah akhirnya benar atau salah, prosesnya bisa menghasilkan wawasan baru.

• Sepertinya versi matematika dari 《The Ballad of John Henry》 juga akan ditulis oleh AI. Saya penasaran siapa juara manusia terakhir yang akan menghasilkan pembuktian “layak masuk THE BOOK” yang bahkan mesin pun tidak bisa melampaui.
  https://en.wikipedia.org/wiki/John_Henry_(folklore)
  https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK

  • Ini adalah cara pandang yang tidak sehat, seperti penggemar sepak bola yang melihat matematika sebagai kompetisi. Hal paling bernilai dalam matematika bukan hanya pembuktian yang indah, melainkan juga definisi yang berguna; membuat definisi yang baik dan dugaan yang baik darinya adalah wilayah yang belum tampak hendak ditaklukkan LLM.
  • Belum sedramatis itu, tetapi ada kemungkinan kita akan segera mencapai tahap tersebut. Kita tidak punya dasar untuk memprediksi secara struktural apakah kemampuan AI akan berkembang secara asimtotik atau berakselerasi, dan kedua kemungkinan tetap terbuka soal masalah mana yang akan terselesaikan oleh metode baru.
    Kita tidak memahami bagian dalam kemampuan AI maupun kurva pertumbuhannya, bahkan tidak benar-benar tahu apakah kinerjanya sengaja ditampilkan lebih rendah. Ini bisa saja fenomena emergen yang menolak pengukuran, atau beberapa tahun lagi menjadi dapat diprediksi seperti jam. Tidak ada yang tahu; kalaupun ada, mereka tidak mengatakannya, dan orang-orang yang bersuara paling lantang pun tidak tahu.

• Jika secara signifikan mempercepat capaian bermakna mahasiswa pascasarjana, tidak ada alasan untuk tidak menginvestasikan $2.400 per tahun per mahasiswa. Dalam keseluruhan biaya, itu nyaris uang receh

  • Sebagian mahasiswa pascasarjana memandang diri mereka bukan sebagai “mesin yang menghasilkan hasil bermakna”, melainkan sebagai makhluk etis. Semua orang tahu bahwa LLM yang berguna sekalipun sulit dibenarkan karena data pelatihan yang dicuri dan dampak lingkungan yang sangat besar
  • Tunjangan biaya hidup untuk program doktor EPSRC sekitar £20.000, jadi jumlah itu setara sekitar 10% dari biaya tahunan. Bagi mahasiswa secara pribadi, itu beban besar

• Seandainya saat kuliah dulu ada formalisasi Lean yang dibuat LLM, itu akan menyenangkan. Matematika di slide kuliah banyak salahnya, dan beberapa profesor menolak permintaan penjelasan dengan berkata “buktinya ada di slide”, sambil tetap enggan mengakui kesalahan
  Bukti Lean itu sendiri sering kali tidak cocok untuk dipahami, tetapi saya berharap dari situ bisa dihasilkan argumen yang mudah dipahami manusia

  • Sulit menyetujui klaim pertama. Kurva belajarnya curam, tetapi formalisasi Lean·Agda·Rocq yang ditulis dengan baik sangat unggul untuk memahami bukti. Formalisasi yang baik menunjukkan ikhtisar dan argumen inti secara terstruktur, dan berbeda dari bukti di atas kertas, memungkinkan kita memeriksa detail setiap langkah sampai kedalaman yang diinginkan
    Repositori TypeTopology Agda milik Martín Escardó adalah contoh yang bagus. Sebaliknya, formalisasi yang dibuat LLM saat ini bisa sangat berantakan; sekalipun mengesahkan kebenaran dan memuat argumen yang menarik, perlu banyak pekerjaan untuk merapikannya agar meningkatkan pemahaman matematis. Tutorial Agda interaktif ada di lets-play-agda.quasicoherent.io
  • Formalisasi juga bisa dipakai untuk pendekatan ala Leibniz yang mengakhiri perdebatan dan sepenuhnya menghilangkan keraguan

• Saya penasaran, bagi matematikawan, apakah kontra-contoh itu seperti hasil tak terduga dalam ilmu fisika—merepotkan saat ini tetapi bisa sangat penting karena mengungkap ketidakakuratan model—atau seperti laporan bug dalam pemrograman, yakni detail kecil yang sepele dan menyebalkan

  • Kontra-contoh memperjelas peran kondisi. Jika ada kontra-contoh yang paling sederhana dan mudah diingat yang menunjukkan apa yang gagal ketika tiap kondisi dalam suatu bukti dilanggar, itu sangat berguna
    Matematikawan cenderung membawa kebun binatang kontra-contoh di kepala mereka. Saat memulihkan suatu teorema pun, mereka dapat mengingat kontra-contoh yang tajam dan berkesan, lalu mempersempit domain dan kondisi agar mengecualikannya
  • Ada buku ajar seperti 《Counterexamples in Topology》 dan 《Counterexamples in Analysis》 yang mengajarkan nuansa suatu bidang melalui kontra-contoh. Buku-buku itu populer karena detail lebih mudah dipelajari dari contoh patologis dan terdegenerasi daripada hanya mempelajari objek normal yang dimaksudkan

• Sebagian besar matematika ini sulit dipahami, tetapi tampaknya umumnya berurusan dengan pembuktian teorema. Jika matematika AI terus berakselerasi, saya penasaran apakah kelak ia juga akan menemukan matematika baru yang diterapkan pada rekayasa atau biomedis, apakah kita berada tepat di ambang terobosan besar umat manusia, atau apakah ia hanya akan membuktikan hal-hal yang sudah diketahui

  • Ada kemungkinan. Compressed sensing bisa dilihat sebagai contoh matematika baru yang diterapkan dalam biomedis, dan dapat sangat mengurangi waktu pemindaian MRI sehingga meningkatkan pengalaman pasien dan memungkinkan lebih banyak pasien menjalani pemeriksaan
    https://en.wikipedia.org/wiki/Compressed_sensing
  • Meski penerapannya di rekayasa dan biomedis mungkin masih jangka panjang, perkembangan metode matematika baru bisa lebih cepat menjadi penting bagi riset fisika fundamental. Beberapa kali, model kosmos meningkat besar setelah muncul alat matematika yang memungkinkan model itu direpresentasikan atau diverifikasi
  • Kalaupun mungkin, itu akan memakan waktu sangat lama. Di sebagian besar bidang terapan, bahkan matematika dari ratusan tahun lalu pun baru sekarang mulai dimanfaatkan dengan benar

• Suatu hari nanti, matematikawan bisa terkubur dalam bukti yang harus ditinjau, dan proposisi palsu yang terlalu dipercaya bisa masuk ke dunia matematika. Matematikawan masa depan mungkin akan seperti software engineer yang memakai AI: memeriksa ribuan baris bukti buatan AI untuk mencari kesalahan halus

  • Titik itu sudah lama terlewati. Literatur saat ini sangat luas dan penuh dengan bukti yang keliru, dan di antara hasil yang diterbitkan pun, meski jumlahnya tidak diketahui tetapi jelas bukan nol, ada hasil palsu yang tercampur