- Lean คือภาษาโปรแกรมที่ออกแบบมาเพื่อให้สามารถทำให้คณิตศาสตร์เป็นทางการได้ และทำให้นักคณิตศาสตร์สามารถจัดการกับทฤษฎีคณิตศาสตร์ในลักษณะเหมือนโค้ดได้
- ผู้ใช้จะเขียน ทฤษฎี, การพิสูจน์, อสมมติฐาน ในรูปแบบโค้ด และกระบวนการพิสูจน์ดำเนินผ่านชุดคำสั่งที่เรียกว่า tactic
- แม้การพิสูจน์ยังไม่สมบูรณ์ ก็สามารถปิดชั่วคราวด้วย
sorry ได้ แต่สิ่งนี้เป็น การพิสูจน์เทียม ที่เปรียบได้กับ any ใน TypeScript
- หากเพิ่มอสมมติฐานที่ไม่ถูกต้อง (เช่น
2 = 3) จะก่อให้เกิดความเสี่ยงเรื่องความขัดแย้งทางตรรกะ และความเป็นไปได้ในการพิสูจน์ ข้อกล่าวทุกข้อ
- Lean จะสรุปผลได้เฉพาะจากอสมมติฐานที่เลือกแบบมีเหตุผลและโครงสร้างการพิสูจน์ จึงมีความสำคัญอย่างยิ่งในการรักษาความถูกต้องทางคณิตศาสตร์
Lean: ภาษาสำหรับจัดการคณิตศาสตร์เป็นโค้ด
- Lean คือภาษาโปรแกรมเฉพาะทางที่ออกแบบมาเพื่อเขียนคณิตศาสตร์ที่เป็นทางการ
- นักคณิตศาสตร์ใช้ Lean เพื่อ แสดงคณิตศาสตร์เป็นโค้ด และสามารถจัดโครงสร้าง ทฤษฎีและการพิสูจน์ ของกันและกันเพื่อการทำงานร่วมกันและการแบ่งปันได้
- ชี้ให้เห็นอนาคตที่ความรู้คณิตศาสตร์จำนวนมากของมนุษยชาติจะกลายเป็นรูปแบบโค้ดที่สามารถตรวจสอบและประกอบเข้าด้วยกันแบบกลไกได้
ก้าวแรกของการพิสูจน์ด้วย Lean
- ใน Lean สามารถประกาศทฤษฎีอย่างง่ายได้ด้วยรูปแบบ
theorem two_eq_two : 2 = 2 := by sorry
- เมื่อการพิสูจน์ยังไม่เสร็จ สามารถใส่
sorry เพื่อแก้ปัญหาชั่วคราว แต่ไม่ใช่การพิสูจน์จริง
sorry ทำให้ผ่านการตรวจสอบการพิสูจน์ของ Lean แต่ในเชิงตรรกะไม่สามารถเชื่อถือได้
- เพื่อให้ได้การพิสูจน์ที่สมบูรณ์ ให้ใช้ tactic อย่าง
rfl (reflexivity) เพื่อพิสูจน์สมการที่เป็นเรื่องง่าย อย่างเช่น 2 = 2
- เนื้อหาที่พิสูจน์แล้วสามารถนำไปใช้ซ้ำในทฤษฎีอื่นผ่าน
exact ฯลฯ จึงเน้นย้ำเรื่อง โมดูลาร์
อสมมติฐานและความขัดแย้ง: เมื่อคณิตศาสตร์ถูกทำให้หลอกหลอน
- หากเพิ่มอสมมติฐานเช่น
axiom math_is_haunted : 2 = 3 ลงไป, Lean จะถือว่าเป็นเรื่องจริง
- อสมมติฐานนี้สามารถนำไปใช้ในขั้นตอนการพิสูจน์ถัดไป ทำให้สามารถพิสูจน์ผลลัพธ์ที่ไม่สมเหตุสมผลทางคณิตศาสตร์ได้ด้วย (เช่น
2 + 2 = 6)
- เป็นไปได้ที่จะใช้ tactic
rewrite เพื่อแทนที่ 2 ด้วย 3 และปิดขั้นตอนการพิสูจน์สมการด้วย rfl
- หากอสมมติฐานที่ไม่เหมาะสมก่อให้เกิดความขัดแย้ง, ใน Lean ก็จะเกิดสถานะที่สามารถพิสูจน์ ทุกข้อเสนอ ได้ (ระบบตรรกะพัง)
- ในความเป็นจริง, ในช่วงต้นศตวรรษที่ 20 ความขัดแย้งในระบบอสมมติฐาน เช่น พาราโดกซ์ของ Russell ได้นำไปสู่การพิจารณาเชิงรากฐานของคณิตศาสตร์
- อย่างไรก็ตาม, Lean แสดงให้เห็นอย่างชัดเจนว่าการเลือกอสมมติฐานเป็นเรื่องสำคัญในการคงไว้ซึ่งความชอบธรรมของระบบตรรกะ
Lean ในฐานะ Proof Checker
- หากคัดเลือกอสมมติฐานอย่างเหมาะสมและ Lean ถูกต้องตามตรรกะ จะให้ข้อสรุปที่น่าเชื่อถือในทางทฤษฎี
- จากสมการง่ายไปจนถึงทฤษฎีที่ซับซ้อนมาก (เช่น Fermat’s Last Theorem) ก็ตรวจสอบได้ตามหลักการเดียวกันทั้งหมด
- ทฤษฎีขนาดใหญ่มีลักษณะเป็นต้นไม้ที่เสร็จสมบูรณ์ผ่านการสะสมการพิสูจน์ทฤษฎีย่อยและทฤษฎีย่อยต่อเนื่องแบบซ้ำๆ
- ตัวอย่างเช่น มีโครงการขนาดใหญ่ที่กำลัง formalize Fermat's Last Theorem ใน Lean และมีแผนจะมีระบบการพิสูจน์อย่างเป็นทางการโดยไม่มีการใช้
sorry ชั่วคราวในที่สุด
ความสนุกของการเรียนรู้ Lean
- การพิสูจน์ด้วย Lean คือการผสมผสานที่สร้างสรรค์ระหว่างการเขียนโค้ดและคณิตศาสตร์
- ตั้งแต่การพิสูจน์ข้อเสนอง่าย ๆ ในขั้นแรก ค่อย ๆ สะสมการก่อสร้างคณิตศาสตร์ที่ซับซ้อนและลึกซึ้งอย่างเคร่งครัด ซึ่งเป็นความสนุกสำคัญ
- คู่มือทางการและทรัพยากรชุมชน (เช่น Natural Numbers Game, Mathematics in Lean ฯลฯ) เหมาะสมสำหรับผู้เริ่มต้น
- การใช้ Lean ทำให้คุณ formalize ตรรกะด้วยตัวเอง และทำให้ได้ค้นพบเสน่ห์ของไอเดียแยบยลกับความงดงามของการโต้แย้งอีกครั้ง
- บทความสรุปว่าบางกลุ่มคนแม้ไม่มีเหตุผลชัดเจน ก็ยังรู้สึกว่า Lean ให้ความสนุกที่เป็นพิเศษ
ยังไม่มีความคิดเห็น