Առաջարկեք ձեր պնդումը։ Կարմիր գիծը որոշում է, թե արդյոք այն ապացուցված է։

Մասնավորապես, մոդելների մի խումբ գրականության, SageMath, PARI/GP և SMT լուծման միջոցների միջոցով հարձակվում է ձեր խնդիրների վրա, ապա ֆորմալացնում է արդյունքը Lean 4-ի և Mathlib-ի միջև։ Lean-ի հիմքը կամ ընդունում է ապացույցը, կամ չի ընդունում այն, և ոչ մի վստահելի բանաստեղծություն չի կարող փոխել դա։ Երբ այն ձախողվում է, դուք ստանում եք ճիշտ նպատակը, որը մնում է, որը սովորաբար այն է, որտեղ անուղղակի վիճաբանությունը ձեռքի շարժումն է։

Գործողություն

Պարզեք, թե ինչ է նշանակում done. «Այստեղ որոշեք, թե X-ը ճիշտ է, և ապացուցեք, որ այն ավելի լավ է, քան «պատմեք X-ի մասին»։

Ցուցակ, որը պետք է մաքրել

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.

Դատավորը բառացիորեն պահում է այս քարտը։ Պահանջեք մրցանակի մակարդակի ապացույց և այն պարզապես կհայտնի ձեզ, երբ խումբը պարտվում է, ոչ թե հաղթանակը կհայտարարի։

Պլանշետը

Ավելի շատ տեղեր նշանակում է ավելի շատ անկյուններ, և ավելի շատ գումար յուրաքանչյուր ռաունդի համար։

Խաղացող

Rules on the criteria and re-checks every piece of evidence. Worth your strongest model.

Ընդմիջում

Օրվա ավարտը

Այն հարվածելը կանգ է առնում խաղը։ Ոչինչ չի կորչում։

Տեսանելիություն

Հրապարակել, երբ ավարտվել է

Գրանցվել խաղ սկսելու համար

Նոր հաշիվները սկզբնական վարկ են ստանում, որը բավական է իրական խաղի համար։

Պարզաբանող, որը չի կարող համոզվել

Lean 4-ը Mathlib-ի հետ ստուգում է վերջնական հայտարարությունը, և ապացուցումը, որը հիմնված է sorry, native_decide կամ նոր ակսիոմի վրա, մերժվում է հաշվարկելու փոխարեն։ Նրա կողքին են SageMath, PARI/GP, Z3, CVC5 և OEIS-ը, այնպես որ կառույցը կարող է հաշվարկվել և հայտնաբերվել, մինչև որևէ մեկը փորձի ապացուցել դրա մասին ինչ-որ բան։

Անհաջող ապացույցը հայտնաբերում է

Երբ ֆորմալացումը ձախողվում է, նպատակը, որը Lean-ը չի կարողացել փակել, փոխանցվում է այն տեղին, որը լավագույնս կարող է աջակցել դրան՝ միայն այդ նպատակը, ոչ թե ամբողջ պատմությունը։ Քննարկված ապացույցը ճշգրիտ անվանում է բացը, ինչը ավելին է, քան շատ անformal arguments երբևէ անում են։

Ոչինչ չի ապացուցվում երկու անգամ։

Յուրաքանչյուր լեմմա, որը ցուցակը հաստատում է, գնում է կիսաշրջանառության գրադարան իր ապացույցով, այնպես որ այն երբեք չի վերարտադրվում և փակուղիները երբեք չեն փորձվում։ Ժամանակակից խնդիրները դադարում են և վերսկսվում առանց աշխատանքի կորստի. փակեք վահանակն ու վերադառնաք վաղը։