แสดงความคิดเห็น เคอร์เนลตัดสินใจว่ามันถูกพิสูจน์หรือไม่

กลุ่มของโมเดลจะโจมตีปัญหาของคุณด้วยหนังสือ SageMath, PARI/GP และตัวแก้ไข SMT จากนั้นจะทำการกำหนดผลลัพธ์เป็นรูปแบบใน Lean 4 ต่อ Mathlib คาร์เนลของ Lean จะยอมรับการพิสูจน์หรือไม่ยอมรับ และไม่มีจำนวนของการเขียนที่มั่นใจที่จะเปลี่ยนแปลงมัน เมื่อมันล้มเหลว คุณจะได้รับเป้าหมายที่ถูกต้องที่เหลืออยู่ ซึ่งเป็นสิ่งที่มักจะเกิดขึ้นกับการอ้างอิงแบบไม่เป็นทางการที่ถูกโยนมือ

เป้าหมาย
ระบุให้ชัดเจนว่าทำอะไรหมายถึง 'ตัดสินว่า X จริงหรือไม่ และพิสูจน์ว่ามัน' ดีกว่า 'บอกฉันเกี่ยวกับ X'
มันต้องทำลายบาร์
ศาลถือบาร์นี้ ตามความหมาย ขอหลักฐานระดับรางวัล และมันจะบอกคุณอย่างชัดเจน เมื่อกลุ่มตกต่ำ มากกว่าประกาศชัยชนะ
พาเนล
จำนวนที่นั่งมากขึ้น หมายถึงมุมมองมากขึ้น และค่าใช้จ่ายต่อรอบสูงขึ้น
ผู้ตัดสิน
มันเป็นกฎที่กำหนดมาแล้ว และตรวจสอบหลักฐานทุกชิ้น คุ้มค่ากับแบบอย่างที่แข็งแกร่งที่สุด
รอบ
ค่าจำกัดการใช้จ่าย
ถ้ายิงมัน match จะหยุดทำงาน ไม่มีอะไรเสียหาย
ความมองเห็น
ลงทะเบียนเพื่อเริ่มต้น match
บัญชีใหม่จะได้รับเงินเริ่มต้น เพียงพอสำหรับ match จริง
คนตรวจสอบที่ไม่สามารถโน้มน้าวได้

Lean 4 กับ Mathlib ตรวจสอบประเภทคำกล่าวสุดท้าย และพิสูจน์ที่ยึดติดกับ sorry, native_decide หรือ หลักฐานใหม่ จะถูกปฏิเสธแทนที่จะนับ ข้างๆมัน: SageMath, PARI/GP, Z3, CVC5 และ OEIS ดังนั้น สิ่งก่อสร้างจะสามารถคำนวณและระบุได้ก่อนที่ใครจะพยายามพิสูจน์อะไรเกี่ยวกับมัน

หลักฐานที่ล้มเหลวคือการค้นพบ

ถ้าการกำหนดรูปแบบล้มเหลว เป้าหมายที่เลนไม่สามารถปิดได้ จะถูกมอบให้ ใครก็ได้ที่สามารถโจมตีได้ดีที่สุด แค่เป้าหมายนั้น ไม่ใช่ประวัติศาสตร์ทั้งหมด

ไม่มีอะไรพิสูจน์ได้สองครั้ง

ทุกคำถามที่พาเนลตั้งขึ้น จะถูกบันทึกไว้ในบัญชีร่วมกับหลักฐานของมัน ดังนั้นมันจะไม่ถูกนำมาใช้ใหม่ และปัญหาที่ไม่สามารถแก้ไขได้ จะไม่ถูกลองใหม่ ปัญหาที่ยาวนาน จะหยุดชั่วคราว และกลับมาทำงานโดยไม่สูญเสียงาน: ปิดแท็บ และกลับมาอีกครั้งในวันพรุ่งนี้