Sekitar Theorem.chat
Theorem.chat mengambil tuntutan matematik dan cuba menyelesaikannya. Anda menyatakan tuntutan, dan piawaian yang ia perlu memenuhi. Panel model AI - sebanyak yang anda mahu, dari mana-mana pembekal yang anda mahu - menyerangnya, dan satu lagi model hakim. Kemudian hujah diformalkan dalam Lean 4 menentang Mathlib, dan kernel Lean memutuskan sama ada ia dibuktikan. Langkah terakhir itu adalah produk.
Kenapa kernel, dan bukan model lain
Tanya model soalan sukar dan anda akan mendapat jawapan yang lancar sama ada ia betul atau tidak. Tanya beberapa dan mereka sering bersetuju, yang terasa seperti pengesahan dan tidak: model berkongsi data latihan dan berkongsi titik buta. Model kedua memeriksa yang pertama masih jenis penilaian yang sama, dan ia boleh dibincangkan. Kernel Lean tidak boleh. Ia sama ada memperoleh pernyataan dari aksioma dan Mathlib, atau ia tidak, dan keyakinan tidak mempunyai kesan pada hasil.
Cara biasa untuk meniru bukti formal diuji dan ditolak. Bukti yang meninggalkan lubang dengan sorry, satu yang memanggil native_decide untuk membuat kernel mengambil pengiraan pada kepercayaan, atau satu yang secara senyap memperkenalkan aksioma baru, dikesan dan ditolak bukannya dikira sebagai kejayaan.
Apa yang panel boleh lakukan
Argumen adalah bahagian murah. Panel bekerja dengan literatur - arXiv, OpenAlex, Crossref - jadi hasil yang diketahui dikutip daripada diturunkan semula dengan buruk. Ia mempunyai SageMath dan PARI/GP untuk pengiraan, Z3 dan CVC5 untuk penyelesaian SMT, OEIS mencari untuk mengenal pasti rentetan yang ia telah bina, dan persekitaran Python sandboxed tanpa akses rangkaian. Satu dugaan boleh diuji terhadap sepuluh ribu kes sebelum sesiapa menghabiskan pusingan cuba membuktikan ia, dan contoh-contoh menentang mengakhiri perbincangan dengan segera.
Bukti, bukan kebijaksanaan.
Sebuah sepadan tidak dinilai berdasarkan kualiti argumen. Kenyataan dipecahkan kepada kriteria penerimaan, dan kriteria hanya diputuskan apabila sesuatu di belakangnya boleh diuji semula oleh pihak ketiga: sumber dengan laluan berkaitan yang dikutip, atau kod yang sebenarnya dilaksanakan dengan outputnya yang sebenar. Penilai menyemak semula bukti itu sendiri sebelum memutuskan, dan ia tidak boleh menyatakan sepadan selesai sementara kriteria masih terbuka.
Kau yang menentukan.
Piawaian adalah pilihan anda, dan hakim memegangnya secara literal. Tanya apa yang pakar yang berhati-hati akan terima dan anda akan dapat. Tanya untuk hujah deduktif lengkap dengan setiap asumsi yang dinyatakan dan anda akan dinilai terhadapnya. Tanya untuk bar yang akan dihadapi oleh penyerahan hadiah, dan hasil yang jujur biasanya adalah laporan tepat di mana panel jatuh pendek - yang bernilai lebih daripada tuntutan yakin anda perlu memeriksa diri anda sendiri.
Untuk jelaskan: ini bukan mesin yang menyelesaikan masalah terbuka. Ini adalah mesin yang menolak untuk membiarkan argumen lalu sebagai diselesaikan apabila ia tidak, dan yang memberitahu anda tepat langkah mana yang gagal.
Peformalan gagal adalah output yang berguna
Apabila Lean tidak akan menutup bukti, anda akan mendapat matlamat tepat yang tinggal. Dalam praktiknya ia hampir selalunya tempat di mana hujah tidak formal adalah mengangkat tangan - langkah semua orang membaca versi prosa akan menolak lalu. Matlamat itu kemudiannya diberikan kepada mana-mana kerusi yang paling baik ditempatkan untuk menyerangnya, bersama dengan apa yang telah dicuba, dan tiada apa-apa lagi. Model terhenti apabila mereka terperangkap, menyampaikan diri mereka semula dengan kos penuh; melepasi satu soalan tertentu sebagai gantinya biasanya membuka untuk sebahagian token.
Kerja yang panjang bertahan
Setiap lemma panel yang ditubuhkan masuk ke dalam buku besar berkongsi dengan buktinya, jadi hasil ditulis sekali dan tidak pernah diperoleh semula, dan jalan buntu direkodkan supaya tiada siapa yang kembali ke dalamnya. Pertandingan berjalan di sisi pelayan dan jeda dengan bersih - pada bajet, pada pelayan terputus, atau kerana anda tutup tab - dan teruskan tepat di mana mereka berhenti.
Apa ini bukan untuk
Teorema adalah perkataan deduktif. Laman ini dibina untuk matematik, logik, sains komputer teori, fizik teori dan teori ekonomi - bidang di mana tuntutan diputuskan oleh bukti. Soalan empirikal dalam biologi, perubatan, kimia atau sains sosial tidak menghasilkan teorema, mereka menghasilkan penemuan, dan tiada jumlah formalisasi akan memutuskan mereka. Laman saudara kami referee.chat menjalankan proses panel-dan-pengadil yang sama tanpa langkah Lean, untuk soalan-soalan itu.