L-argument jiġi ddikjarat. Il-kernel jiddeċiedi jekk hux ippruvat.

Panel ta’ mudelli jattakkaw il-problema tiegħek bil-letteratura, SageMath, PARI/GP u solver SMT, imbagħad jifformalizza r-riżultat f’Lean 4 kontra Mathlib. Il-kernel ta’ Lean jew jaċċetta l-prova jew ma jaċċettahiex, u l-ebda ammont ta’ prosa kunfidenti ma jbiddel dan. Meta ma jirnexxilux tikseb l-għan eżatt li jibqa’, li normalment huwa fejn l-argument informali kien hand-waving.

L-għan
Kun speċifiku dwar x'ifisser "Deċiedi jekk X hux veru, u ppruvah" tħabbat "għidli dwar X".
Il-bar li għandu ċar
L-arbitru għandu dan il-bar litteralment.Itlob għal prova fil-livell tal-premju u se jgħidlek b'mod ċar meta l-panel jaqa' qasir, aktar milli jiddikjara r-rebħa.
Il-bord
Aktar siġġijiet tfisser angoli aktar, u l-ispiża aktar għal kull round.
Referee
Regoli dwar il-kriterji u re-checks kull biċċa evidenza. Worth mudell qawwija tiegħek.
Rounds
Limitu ta’ nfiq
Li tolqot dan jissospendi l-match. Xejn huwa mitluf.
Viżibbiltà
Irreġistra biex tibda match
Kontijiet ġodda jiksbu kreditu bidu, biżżejjed għal reali match.
A kontrollur li ma jistgħux jiġu persuaded

Lean 4 ma Mathlib tip-iċċekkja l-dikjarazzjoni finali, u prova li tistrieħ fuq sorry, native_decide jew assioma friska hija miċħuda minflok ma jingħaddu.Ma' dan: SageMath, PARI/GP, Z3, CVC5 u l-OEIS, sabiex kostruzzjoni jistgħu jiġu kkalkulati u identifikati qabel xi ħadd jipprova jipprova xi ħaġa dwar dan.

A prova ma rnexxielhomx hija sejba

Meta l-formalizzazzjoni ma tirnexxix, l-għan Lean ma setgħetx tagħlaq hija mogħtija lil kwalunkwe sit li huwa l-aħjar post biex jattakkaw dan: biss dak l-għan, mhux l-istorja kollha.Prova rifjutata jismu l-distakk preċiżament, li huwa aktar minn ħafna argumenti informali qatt ma jagħmlu.

Xejn ma huwa ppruvat darbtejn

Kull lemma l-panel jistabbilixxi tmur f'reġistru kondiviż mal-prova tagħha, sabiex ma tkunx re-derivat u dead ends huma qatt ma jerġgħu jiġu ppruvati.problemi twal jitwaqqfu u jerġgħu jibdew mingħajr ma jitilfu xogħol: tagħlaq it-tab u jerġgħu lura għada.