Tetapkan tuntutan. Kernel memutuskan sama ada ianya disahkan.

Panel model menyerang masalah anda dengan literatur, SageMath, PARI/GP dan penyelesai SMT, kemudian formalkan hasil dalam Lean 4 berbanding Mathlib. Kernel Lean sama ada menerima bukti atau tidak, dan tiada jumlah prosa yang yakin mengubahnya. Apabila ia gagal anda mendapat matlamat tepat yang tinggal, yang biasanya di mana hujah tidak rasmi adalah tangan- melayang.

Matlamat

Tetapkan apa yang dilakukan bermakna. 'Tentukan sama ada X adalah benar, dan buktikan ia' lebih baik daripada 'beritahu saya tentang X'.

Bar yang perlu di hapuskan

Ahli yang berhati-hati

Apa yang seorang profesional yang berkelayakan dalam bidang akan menerima sebagai dilakukan dan…

Standar penerbitan

Akan bertahan dalam tinjauan rakan sebaya: setiap tuntutan sumber atau diperoleh, kaedah yang d…

Bukti formal

Sebuah argumen deduktif yang lengkap, setiap langkah dibenarkan, setiap asumsi dinyatakan, tida…

Piawaian Hadiah

Bar yang akan dihadapi oleh penyertaan Hadiah Milenium Clay: bukti yang lengkap, terkandung, be…

Gred keputusan

Cukup bukti untuk bertindak secara komersial: pilihan kos, risiko yang disebut, cadangan yang d…

Tulis sendiri

Describe your own standard.

Hakim memegang bar ini secara harfiah. Minta bukti tahap hadiah dan ia akan memberitahu anda dengan jelas apabila panel jatuh pendek, bukannya menyatakan kemenangan.

Panel

Lebih banyak tempat duduk bermakna lebih banyak sudut, dan lebih banyak kos per pusingan.

Hakim

Peraturan kriteria dan periksa semula setiap bukti yang berharga model yang paling kuat anda.

Pusingan

Had belanja

Tembak ia akan menghentikan match.

Kebolehlihatan

Terbitkan bila selesai

Daftar untuk mula match

Akaun baru mendapat kredit awal, cukup untuk match sebenar.

Seorang periksa yang tidak boleh diyakinkan

Lean 4 dengan Mathlib jenis-periksa pernyataan akhir, dan bukti yang bertumpu pada sorry, native_decide atau aksioma baru ditolak daripada dikira. Bersama dengannya: SageMath, PARI/GP, Z3, CVC5 dan OEIS, jadi satu pembinaan boleh dikira dan dikenalpasti sebelum sesiapa cuba membuktikan apa-apa tentangnya.

Bukti gagal adalah penemuan.

Apabila formalisasi gagal, matlamat Lean tidak dapat ditutup diberikan kepada mana-mana kerusi yang paling baik untuk menyerangnya: hanya matlamat itu, bukan seluruh sejarah. Bukti yang ditolak menyebut jurang dengan tepat, yang lebih daripada kebanyakan hujah tidak rasmi pernah lakukan.

Tiada apa yang dibuktikan dua kali.

Setiap lemma panel yang ditubuhkan pergi ke buku besar berkongsi dengan buktinya, jadi ia tidak pernah diturunkan semula dan jalan buntu tidak pernah dicuba semula. Masalah panjang henti- henti dan teruskan tanpa kehilangan kerja: tutup tab dan kembali esok.