თჱპვფთ ჟთ ოპჲვკრა. ჟყპუვრჲ ღვ ჲრკპთვ ჟვ ოპჲგვპწგა ლთ.
მოდელის პანელი თავს დაესხმება თქვენს პრობლემას ლიტერატურის, SageMath, PARI/GP და SMT გადაწყვეტილების მეშვეობით, შემდეგ ფორმალიზებს შედეგს Lean 4- ში Mathlib- სთან შედარებით. Lean- ის ბირთვი ან იღებს დადასტურებას ან არ იღებს და არანაირი იმედისმომცემი პროზა არ ცვლის ამას. როდესაც ის ვერ შეძლებს, თქვენ მიიღებთ ზუსტ მიზანს, რომელიც რჩება, რაც ჩვეულებრივ არფორმალური არგუმენტის ხელის ცემას წარმოადგენს.
ფვკთპ, კჲირჲ ნვ მჲზვ ეა ჟვ სბვეთ.
Lean 4 და Mathlib ტიპის შემოწმება მთავრდება და დადასტურება, რომელიც sorry, native_decide ან ახალი აქტიუმის მიხედვით არის, არ ითვლება. მის გვერდით: SageMath, PARI/GP, Z3, CVC5 და OEIS, ასე რომ კონსტრუქცია შეიძლება გამოითვალოს და იდენტიფიცირდეს, სანამ ვინმეს შეეცდება რაიმეს დადასტურება.
ოპჲოსჟნარჲრჲ ეჲკაჱარვლჟრგჲ ვ ჲრკპთრთვ.
ოჲჟლვ ოპჲგალთრვ ნა ოჲპმალთჱაუთწრა, ჱაეყლზვნთვრჲ, კჲვრჲ ნვ მჲზვ ეა ჟვ ჱარგჲპთ, ჟვ ოპვგყპღა გჲ ჟვჟთწ, კჲწრჲ ვ ნაი-ეჲბპვ ოჲჱთუთჲნთპანა ეა დჲ ჲბყპნვ: ჟამჲ ჱაეყლზვნთვრჲ, ნვ თ ჟთრვ თჟრჲპთთ. ჲრჳგყპლვნთრვ ეჲკაჱანთწ ოპვუვნრწრ ოპვკპაჟთრვ, კჲთრჲ ჟა ოჲგვფვ ჲრ ნვჲტთუთალნთრვ აპდსმვნრთ.
ნთღჲ ნვ ჟვ ეჲკაჱგა ეგა ოყრთ.
ყველა ლემა, რომელიც პანელმა დაამტკიცა, ხვდება საჯარო წიგნაკში თავისი დადასტურებით, ასე რომ ის არასდროს არ არის აღდგენილი და უსასრულო წერტილები არასდროს არ არის განმეორებითი. გრძელი პრობლემები შეჩერებულია და აღდგება სამუშაოს დაკარგვის გარეშე: დახურეთ ჩანართი და დაბრუნდით ხვალ.