İddiayı söyleyin.

Bir model paneli, literatür, SageMath, PARI/GP ve bir SMT çözümleyici ile sorununuza saldırır, sonra sonucu Lean 4'e karşı Mathlib'de resmileştirir. Lean'ın çekirdeği kanıtı ya kabul eder ya da kabul etmez, ve hiçbir güvenilir metin bu durumu değiştirmez. Başarısız olduğunda, geri kalan doğru hedefi alırsınız, ki bu genellikle gayri resmi argümanın el sallama olduğu yerdir.

Amaç
Yapılan şeyin ne anlama geldiğine dair açık ol. "X'in doğru olup olmadığına karar ver ve kanıtla" "X hakkında bana söyle"den daha iyidir.
Bar temizlemek zorunda
Hakem bu bardağı gerçekten tutar. ödül seviyesinde bir kanıt isteyin ve panelin başarısız olduğunda size açıkça söyler, zafer ilan etmek yerine.
Panel
Daha fazla koltuk daha fazla açı demektir ve tur başına daha fazla maliyet.
Hakem
Kriterleri belirler ve her kanıt parçasını tekrar kontrol eder. en güçlü modelin değerinde.
Turlar
Harcama limiti
Ona vursan match'i durdurursun.
Görünürlük
match'i başlatmak için kayıt olun
Yeni hesaplar kredi alıyor, gerçek match'e yetecek kadar.
İzin verilmeyen bir kontrolcü

Lean 4 ile Mathlib son ifadeyi tip-kontrol eder ve sorry, native_decide veya yeni bir aksiyoma dayanan bir kanıt sayılma yerine reddedilir. Yanında: SageMath, PARI/GP, Z3, CVC5 ve OEIS, böylece bir yapı, herhangi biri onun hakkında bir şeyi kanıtlamaya çalışmadan önce hesaplanarak tanımlanabilir.

Başarısız kanıt bir bulgudur.

Formalizasyon başarısız olduğunda, Lean'ın yaklaşamaması gereken hedef, ona saldırmak için en iyi konumda olan yere verilir: sadece o hedef, tüm tarih değil. Reddedilen bir kanıt boşluğu kesin olarak adlandırır, ki bu çoğu gayriresmi argümandan daha fazlasını yapar.

Hiçbir şey iki kez kanıtlanmaz.

Panelin belirlediği her lemma kanıtı ile birlikte paylaşılan bir defter içinde olur, böylece hiçbir zaman tekrar türetilmez ve çıkmaz noktalar hiçbir zaman tekrar denetlenmez. Uzun sorunlar çalışma kaybetmeden durdurulur ve devam eder: sekmeyi kapatın ve yarın geri gelin.