Bu sözi aýt. Kernel bu sözi islemese-de kabul eder.

Model paneli siziň problemaňyza edebiýat, SageMath, PARI/GP we SMT çözgüç bilen hüjüm eder, soňra netijäni Lean 4 we Mathlib arasynda resmileşdirer. Lean's kernel ýa ispat kabul eder ýa ispat etmeýär, we hiç bir mukdarda ynamly proza buny üýtgetmez. Eger ol hata ederse, siz galkan dogry maksaty alarsyňyz, bu adatça resmi bolmadyk argümentiň el-waşlamak ýeridir.

_Gün
Dogry edileni nädip düşündirmelidigini belli ediň. 'X' aňsatmy ýa-da dälmi karar beriň, we buny subut ediň' beats 'tell me about X'.
Pozmak üçin bar
Reýder bu bary sözme-söz saklaýar. Bir baýragyň derejesi üçin delil soraň we paneliň az galanda size aç-açan aýtjak, ýeňiş yglan etmekden başga.
Panel
Ene
Rejim
Bu algoritm, umumy we umumy däl algoritmleri birikdirmek üçin ulanylýar.
_Gün
Spending limit
Ony basmak match'i durdurýar. Hiç zat ýitmedi.
Görkez
match başlamak üçin ýaz
Täze hasaplar başlatma kreditini alar, hakykat match üçin ýeterlik.
Bir barlagçy, ol öwürilip bilmez

Lean 4 with Mathlib type-checks the final statement, and a proof that relies on sorry, native_decide or a fresh axiom is rejected rather than counted. Together with it: SageMath, PARI/GP, Z3, CVC5 and the OEIS, so a construction can be calculated and identified before anyone tries to prove anything about it.

A failed proof is a finding

Formalization batly bolmadyk wagty, Lean's nädip ýapmak başarmadyk maksat, oňa hüjüm etmek üçin iň gowy ýere geçýär: diňe bu maksat, ähli geçmiş däl. Rejected evidence names the gap precisely, which is more than most informal arguments ever do.

Hiç zat iki gezek subut edilmez

Paneliň düzýän her bir lemmasy onuň subutnamasy bilen paýlaşylan bir kitapçada gidýär, şonuň üçin ol hiç wagt tekrardan alnanok we ölüň aýaklary hiç wagt tekrardan synlanok. Uzak mesele iş ýitirmezden durdurylyp dowam eder: täbi bagla we ertir gaýt.