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

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.

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-logħba. Xejn huwa mitluf.

Viżibbiltà

Ippubblika meta lest

Irreġistra biex tibda logħba

Kontijiet ġodda jiksbu kreditu bidu, biżżejjed għal logħba reali.

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.