Astra OpenAI Menyelesaikan Sepuluh Masalah Matematik Terbuka — dan Kisah Sebenarnya Bukan tentang Matematik

Ringkasnya: pada 1 Ogos 2026, OpenAI mengumumkan bahawa versi dalaman model seterusnya, Astra, menghasilkan dapatan baharu bagi sepuluh masalah terbuka dalam matematik dan sains komputer teori, yang setiap satunya tidak dapat diselesaikan sekurang-kurangnya selama sedekad. Lebih penting daripada dapatan itu sendiri ialah cara ia diserahkan: setiap satu disertakan dengan sijil bukti Lean 4 yang boleh disemak oleh mesin di GitHub, bersama manuskrip setebal 249 halaman, dengan jumlah kos pengkomputeran kira-kira USD 2,000. Pengajaran bagi pemilik perniagaan bukan tentang teori kumpulan atau pembungkusan sfera. Ia ialah satu prinsip: AI yang memberikan anda output yang boleh disahkan oleh mesin pada asasnya berbeza daripada AI yang memberikan anda tulisan yang meyakinkan.

Apakah sebenarnya yang diumumkan?

Dapatan utama ialah pembinaan eksplisit pertama bagi apa yang dipanggil kumpulan bukan sofik, satu persoalan yang terbuka sejak Mikhail Gromov memperkenalkan konsep kesofikan pada tahun 1999. Bersamanya ialah sangkalan terhadap konjektur ketegaran Connes tentang aljabar von Neumann, bukti konjektur isi padu Ehrhart, penyelesaian tiga masalah daripada katalog Paul Erdős — termasuk Masalah 183 tentang nombor Ramsey berbilang warna — dan had atas yang lebih baik bagi ketumpatan pembungkusan sfera berdimensi tinggi, yang dilaporkan sebagai penambahbaikan pertama sejak tahun 1978.

Perkara yang membezakan ini daripada gelombang dakwaan "AI telah menyelesaikan satu masalah" sebelum ini ialah cara penyerahannya. Daripada satu dakwaan yang anda diminta percayai, OpenAI menerbitkan sijil Lean 4 bagi setiap dapatan, dengan kiraan "sorry" sifar — penanda teknikal yang bermaksud tiada langkah dalam fail yang diterbitkan dibiarkan tanpa bukti. Sesiapa sahaja yang mempunyai komputer boleh mengklon repositori, menjalankan pemeriksa dan mendapat keputusan muktamad dalam beberapa minit, dan bukannya menunggu berbulan-bulan untuk semakan manual.

Nilainya bukan pada model yang mendakwa satu dapatan. Nilainya ialah model itu turut menyerahkan sebuah mesin yang menyemak dakwaan itu bagi pihak anda.

Sisi lain: kritikan serius yang wajar dinyatakan

Gambarannya tidak cerah sepenuhnya, dan jujurnya perkara itu perlu disebut. Ahli matematik pakar membangkitkan bantahan yang substantif. Pertama, tiada satu pun daripada sepuluh dapatan itu yang telah melalui semakan rakan sebaya, dan pengumumannya dibuat melalui catatan blog syarikat dan bukannya jurnal — yang dilihat oleh sesetengah pihak sebagai bercanggah dengan semangat Deklarasi Leiden yang dikeluarkan pada Jun 2026. Kedua, terdapat dakwaan tentang ketiadaan atribusi kepada kerja terdahulu: penyelidik menegaskan bahawa hujah pembungkusan sfera menggunakan semula aliran penaakulan yang telah diterbitkan sebelum ini tanpa memberikan pengiktirafan, dan corak yang sama juga dikesan dalam dapatan kumpulan bukan sofik.

Terdapat juga kaveat teknikal yang penting. Lean menghapuskan pelbagai jenis ralat logik setempat, tetapi ia tidak menukar definisi — atau terjemahan soalan matematik tidak formal kepada pernyataan formal — menjadi fakta mekanikal. Secara mudahnya: sesuatu bukti boleh betul sepenuhnya sedangkan pernyataan yang dibuktikan tidak sepadan dengan soalan yang dipercayai orang telah dijawab. Repositori itu sendiri menyifatkan kerja ini sebagai "disemak oleh ejen" dan bukannya disemak secara bebas oleh manusia.

Terjemahan praktikal untuk perniagaan Saudi

Jarak antara satu persoalan dalam teori kumpulan dengan kedai, kilang atau syarikat perkhidmatan anda mungkin kelihatan sangat jauh. Namun idea terasnya boleh dipindahkan secara langsung, kerana output AI terbahagi kepada dua kategori yang memerlukan pengurusan risiko yang sama sekali berbeza:

  • Output yang boleh disahkan oleh mesin: kod yang lulus ujian, catatan jurnal yang seimbang, invois yang diterima oleh platform e-invois, pertanyaan pangkalan data yang hasilnya boleh anda selaraskan dengan sumber rujukan. Di sini anda boleh membiarkan model bergerak pantas, kerana ada hakim terakhir yang tidak mengampu.
  • Output yang tidak boleh disahkan: ringkasan mesyuarat, jawapan kepada pelanggan, analisis pasaran, cadangan pengambilan pekerja. Tiada pemeriksa yang memberikan keputusan lulus atau gagal, jadi anda memerlukan semakan manusia, sumber yang kelihatan dan had yang jelas tentang perkara yang dibenarkan untuk didakwa oleh model.

Projek AI yang paling teruk gagal dalam syarikat ialah projek yang melayan kategori kedua seolah-olah kategori pertama. Sebaliknya juga benar: banyak peluang yang menguntungkan terlepas kerana tiada sesiapa perasan bahawa sesuatu proses sebenarnya membolehkan pengesahan automatik jika direka bentuk dengan betul.

Cara membina lapisan pengesahan dalam syarikat anda

Langkah pertama ialah bertanya, bagi setiap proses yang anda pertimbangkan untuk diautomasikan: ujian apakah yang membuktikan output itu betul tanpa perlu dibaca oleh manusia? Jika ada jawapannya, anda mempunyai calon automasi yang sangat baik. Jika tiada, anda sama ada mereka bentuk ujian sedemikian atau mengekalkan manusia dalam gelung proses.

Dalam sistem perniagaan, ini bermaksud perkara yang konkrit: peraturan pengesahan yang dikuatkuasakan di peringkat pangkalan data dan bukan hanya di antara muka pengguna; pemadanan tiga hala automatik antara pesanan, invois dan inventori; penyelarasan output model dengan satu sumber kebenaran sebelum ia dipercayai; ujian automatik yang dijalankan pada setiap perubahan kod; dan jejak audit yang menunjukkan siapa menghasilkan apa, bila dan daripada data mana. Ini bukan kemewahan kejuruteraan — inilah yang menjadikan penggunaan AI dalam operasi sensitif boleh dipertahankan di hadapan juruaudit, pelanggan dan pengawal selia anda.

Jangan juga abaikan dimensi kawal selia. Sebarang pemprosesan data peribadi di Kerajaan Arab Saudi tertakluk kepada Undang-undang Perlindungan Data Peribadi (PDPL), dan prinsip had tujuan, peminimuman data serta akauntabilitinya bermaksud secara praktikal bahawa anda memerlukan rekod berdokumen tentang apa yang dilakukan oleh model — bukan sekadar keyakinan terhadap kualitinya.

Tiga pengajaran untuk dibawa bersama

Pertama, keupayaan penaakulan mendalam berkembang lebih pantas daripada yang diandaikan oleh banyak pelan hala tuju syarikat, dengan kos operasi yang menurun dengan cepat — USD 2,000 untuk sepuluh dapatan bertaraf penyelidikan ialah angka yang wajar direnungkan. Kedua, pengesahan, bukan kepercayaan, yang menukar keupayaan model kepada nilai operasi yang boleh anda harapkan. Ketiga, ketelusan tentang sumber dan atribusi kini sebahagian daripada kualiti output itu sendiri, bukan tambahan kosmetik — dan di situlah tepatnya kritikan minggu ini tertumpu.

Cara kami membinanya di Origami

Kami ialah sebuah syarikat teknologi, dan kerja AI kami bermula daripada soalan yang sama: di manakah output boleh disahkan secara automatik, dan di manakah tidak? Kami mereka bentuk sistem supaya model beroperasi dalam sempadan yang jelas, outputnya melalui peraturan pengesahan dan sumber kebenaran dalam sistem anda sendiri, dan setiap langkah meninggalkan rekod. Matlamatnya bukan model yang lebih pintar — tetapi proses yang boleh anda percayai kerana anda boleh memeriksanya.

Sumber

  • Pengumuman rasmi OpenAI: openai.com
  • Liputan The Next Web, termasuk butiran tentang kumpulan bukan sofik: thenextweb.com
  • SiliconANGLE tentang dapatan dan bukti yang diterbitkan: siliconangle.com
  • Pihak Berkuasa Data dan Kecerdasan Buatan Saudi (SDAIA) — Undang-undang Perlindungan Data Peribadi (PDPL): sdaia.gov.sa