Menyelesaikan setiap masalah dalam salah satu tolok ukur matematika paling berat biasanya memerlukan biaya puluhan ribu dolar. NEAR AI baru saja melakukannya dengan biaya $111.
Pada 6 September 2026, salah satu pendiri NEAR Protocol, Alex Skidanov, mengumumkan bahwa agen open-source Lean dari proyek tersebut telah menyelesaikan semua 672 soal dalam benchmark PutnamBench, sekumpulan soal yang diambil dari Kompetisi Matematika William Lowell Putnam. Total biaya: $111. Submisi termurah kedua yang diketahui harganya 250 kali lebih mahal.
Apa itu PutnamBench, dan mengapa hal ini penting
Kompetisi Putnam adalah kontes matematika sarjana paling bergengsi di Amerika Utara. Mendapatkan skor nol bukan hal yang tidak biasa, bahkan di kalangan siswa brilian. Ujian ini dirancang untuk menghancurkan Anda.
PutnamBench, yang diperkenalkan pada 2024, mengambil tradisi kesulitan tersebut dan menjadikannya seperangkat evaluasi formal untuk pembuktian teorema AI. Benchmark ini berisi 672 soal yang dienkod dalam Lean 4, bahasa asisten bukti yang mengharuskan argumen matematis ditulis dengan presisi yang dapat diverifikasi mesin. Bukti yang secara logis tidak rapi akan ditolak sepenuhnya, tanpa poin parsial.
Sebelum hasil NEAR AI, agen yang mencoba PutnamBench sering memerlukan ribuan panggilan inferensi per masalah. Biaya komputasi menumpuk dengan cepat, membuat jalannya seluruh benchmark berada dalam kisaran total pengeluaran $10.000 hingga $25.000 untuk sistem terkemuka.
Agen Lean NEAR AI menyelesaikan seluruh rangkaian 672 soal seharga $111.
Mengapa kesenjangan biaya adalah cerita sebenarnya
Dengan biaya $10.000 hingga $25.000 per satu siklus penuh, hanya sejumlah kecil organisasi yang mampu mengulang, bereksperimen, dan meningkatkan pipeline pembuktian teorema mereka. Dengan biaya $111, perhitungan ini berbalik sepenuhnya.
Kemajuan pesat dalam hasil PutnamBench antara 2025 dan 2026 sudah didorong oleh alur kerja agen yang menggabungkan model bahasa besar dengan mesin pemeriksa bukti Lean. Pendekatan NEAR AI memperluas pola tersebut, tetapi menambahkan lapisan efisiensi yang belum pernah dilihat oleh komunitas benchmark sebelumnya.
NEAR AI menempatkan pencapaian ini dalam visi infrastruktur yang lebih luas yang berpusat pada apa yang disebutnya IronClaw, sebuah kerangka yang berorientasi pada AI rahasia dan dapat diverifikasi. Kemampuan verifikasi formal sesuai langsung dengan kerangka tersebut: jika Anda dapat membuktikan argumen matematis benar pada tingkat mesin, Anda memiliki dasar untuk sistem AI yang outputnya dapat diaudit secara independen, bukan hanya dipercaya tanpa bukti.
Keputusan NEAR Protocol untuk membuat agen Lean bersifat open-source memperkuat signifikansinya. Alat propietaris yang memberikan keunggulan biaya 250x cenderung tetap bersifat propietaris. Membuka sumber agen berarti metodologinya tersedia untuk diperiksa, dikembangkan, dan digunakan oleh siapa pun.