State the claim. The kernel decides whether it is proved.

მოდელის პანელი თავს დაესხმება თქვენს პრობლემას ლიტერატურის, SageMath, PARI/GP და SMT გადაწყვეტილების მეშვეობით, შემდეგ ფორმალიზებს შედეგს Lean 4- ში Mathlib- სთან შედარებით. Lean- ის ბირთვი ან იღებს დადასტურებას ან არ იღებს და არანაირი იმედისმომცემი პროზა არ ცვლის ამას. როდესაც ის ვერ შეძლებს, თქვენ მიიღებთ ზუსტ მიზანს, რომელიც რჩება, რაც ჩვეულებრივ არფორმალური არგუმენტის ხელის ცემას წარმოადგენს.

The goal
Be specific about what done means. 'Decide whether X is true, and prove it' beats 'tell me about X'.
The bar it has to clear
The referee holds this bar literally. Ask for a prize-level proof and it will tell you plainly when the panel falls short, rather than declaring victory.
პანელი
More seats means more angles, and more cost per round.
ჟყეთწრ.
Rules on the criteria and re-checks every piece of evidence. Worth your strongest model.
რიგი
ხარჯვის ლიმიტი
Hitting it pauses the match. Nothing is lost.
ხილვადი
Sign up to start a match
New accounts get starting credit, enough for a real match.
A checker that cannot be persuaded

Lean 4 და Mathlib ტიპის შემოწმება მთავრდება და დადასტურება, რომელიც sorry, native_decide ან ახალი აქტიუმის მიხედვით არის, არ ითვლება. მის გვერდით: SageMath, PARI/GP, Z3, CVC5 და OEIS, ასე რომ კონსტრუქცია შეიძლება გამოითვალოს და იდენტიფიცირდეს, სანამ ვინმეს შეეცდება რაიმეს დადასტურება.

A failed proof is a finding

When formalisation fails, the goal Lean could not close is handed to whichever seat is best placed to attack it: just that goal, not the whole history. A rejected proof names the gap precisely, which is more than most informal arguments ever do.

Nothing is proved twice

ყველა ლემა, რომელიც პანელმა დაამტკიცა, ხვდება საჯარო წიგნაკში თავისი დადასტურებით, ასე რომ ის არასდროს არ არის აღდგენილი და უსასრულო წერტილები არასდროს არ არის განმეორებითი. გრძელი პრობლემები შეჩერებულია და აღდგება სამუშაოს დაკარგვის გარეშე: დახურეთ ჩანართი და დაბრუნდით ხვალ.