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

Careful expert

What a competent professional in the field would accept as done and correct.

Publication standard

Would survive peer review: every claim sourced or derived, methods stated, limitations acknowle…

Formal proof

A complete deductive argument. Every step justified, every assumption stated, no appeals to pla…

Prize standard

The bar a Clay Millennium Prize submission would face: a complete, self-contained, gap-free pro…

Decision-grade

Enough evidence to act on commercially: options costed, risks named, recommendation justified.

Write my own

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 perlawanan.

Kebolehlihatan

Terbitkan bila selesai

Daftar masuk untuk memulakan perlawanan

Akaun baru mendapat kredit awal, cukup untuk perlawanan 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.