ความคืบหน้าการ formalize ทฤษฎีบทสุดท้ายของแฟร์มา
(xenaproject.wordpress.com)- งานย้ายบทพิสูจน์ FLT ไปยัง Lean ดำเนินมาเป็น เดือนที่สอง แล้ว และแม้นิยามของ R และ T ที่จำเป็นต่อทฤษฎีบท “R=T” ของ Wiles ยังไม่เสร็จสมบูรณ์ แต่มีผลลัพธ์หนึ่งในพีชคณิตสลับที่เชิงนามธรรมที่พิสูจน์ได้แล้ว
- เป้าหมายไม่ใช่การทำซ้ำบทพิสูจน์ดั้งเดิมในทศวรรษ 1990 แบบตรงตัว แต่เป็นการสร้าง บทพิสูจน์ที่ถูกทำให้เป็นทั่วไปและเรียบง่ายขึ้น จากงานต่อยอดของ Diamond/Fujiwara, Kisin, Taylor, Scholze และคนอื่น ๆ บน Lean และ mathlib
- ระหว่าง formalize crystalline cohomology ที่จำเป็นต่อบทพิสูจน์สมัยใหม่ พบปัญหาว่า lemma สำคัญในบทความปี 1965 ของ Roby ซึ่งเป็นเอกสารอ้างอิงมาตรฐานของโครงสร้าง divided power ดูเหมือนจะผิด
- Brian Conrad พบบทพิสูจน์ทางเลือกในภาคผนวกของหนังสือ Berthelot-Ogus และ Arthur Ogus ก็ตอบว่าเขารู้วิธีแก้ข้อผิดพลาดในภาคผนวกนั้น ทำให้โปรเจกต์เดินหน้าต่อได้อีกครั้ง
- กรณีนี้แสดงให้เห็นความเสี่ยงที่รายละเอียดบทพิสูจน์ของคณิตศาสตร์สมัยใหม่พึ่งพาความทรงจำของผู้เชี่ยวชาญและความรู้โดยนัย และช่วยตอกย้ำเหตุผลเชิงปฏิบัติว่าควรบันทึกบทพิสูจน์ไว้ในระบบ formal
สถานะปัจจุบันของการย้ายบทพิสูจน์ FLT ไปยัง Lean
- งานสอนคอมพิวเตอร์ให้รู้บทพิสูจน์ทฤษฎีบทสุดท้ายของแฟร์มา (FLT) ดำเนินมาเป็น เดือนที่สอง แล้ว
- ทฤษฎีบท “R=T” ซึ่งเป็นแกนหลักของบทพิสูจน์ของ Wiles ต้องใช้งานจำนวนมากเพื่อให้นิยามใน Lean ว่า R และ T คืออะไร และตอนนี้นิยามทั้งสองยังไม่เสร็จสมบูรณ์
- Andrew Yang นักศึกษาปริญญาเอก ได้พิสูจน์ผลลัพธ์พีชคณิตสลับที่เชิงนามธรรมที่จำเป็นไว้แล้ว
- เป็นผลลัพธ์ในรูปแบบว่า “ถ้าวงแหวนเชิงนามธรรม R และ T เป็นไปตามเงื่อนไขทางเทคนิคหลายข้อ ทั้งสองจะเท่ากัน”
- ฉบับร่างปัจจุบันเผยแพร่เป็น blueprint แล้ว
- ระบบที่ใช้คือ Lean และไลบรารีคณิตศาสตร์ mathlib
- ผู้ที่พอรู้ Lean และทฤษฎีจำนวนสามารถเข้าร่วมได้ผ่าน contribution guidelines, project dashboard, และ issue
เหตุผลที่ไม่ย้ายบทพิสูจน์จากทศวรรษ 1990 แบบตรงตัว
- โปรเจกต์นี้ไม่ได้ formalize บทพิสูจน์ของ Wiles ในทศวรรษ 1990 แบบตรงตัว
- หลังจากนั้น งานของ Diamond/Fujiwara, Kisin, Taylor, Scholze และคนอื่น ๆ ทำให้บทพิสูจน์ถูกทำให้เป็นทั่วไปและเรียบง่ายขึ้น
- เป้าหมายไม่ได้หยุดแค่พิสูจน์ FLT แต่รวมถึงการสร้างผลลัพธ์ที่ทั่วไปและทรงพลังกว่าไว้ภายใน Lean ด้วย
- หากการปฏิวัติคณิตศาสตร์ด้วย AI เกิดขึ้นจริง และ Lean กลายเป็นองค์ประกอบสำคัญ การทำให้คอมพิวเตอร์มีนิยามแกนกลางของทฤษฎีจำนวนสมัยใหม่ในรูปแบบที่เข้าใจได้ก็อาจเป็นประโยชน์
divided powers ที่จำเป็นสำหรับ crystalline cohomology
- บทพิสูจน์ที่จะ formalize ใช้ crystalline cohomology ซึ่งไม่มีในบทพิสูจน์ดั้งเดิมของ Wiles
- ทฤษฎีนี้พัฒนาขึ้นในปารีสช่วงทศวรรษ 1960–70 และ Berthelot วางรากฐานโดยอิงจากแนวคิดของ Grothendieck
- ฟังก์ชันเอ็กซ์โพเนนเชียลและลอการิทึมแบบคลาสสิกมีความสำคัญต่อการทำความเข้าใจเรขาคณิตเชิงอนุพันธ์และ de Rham cohomology แต่ในบริบทเชิงเลขคณิตอย่าง characteristic p จะไม่ทำงานตามเดิม
- divided power structures ที่พัฒนาขึ้นในบทความของ Roby ช่วงทศวรรษ 1960 มีบทบาทสำคัญในการสร้างฟังก์ชันคล้ายกันที่ใช้ได้ในบริบทเชิงเลขคณิต
- หากต้องการสอน crystalline cohomology ให้ Lean ต้อง formalize divided powers ก่อน
ปัญหาในเอกสารของ Roby ที่เผยขึ้นระหว่างทำงานกับ Lean
- Antoine Chambert-Loir และ Maria Ines de Frutos Fernandez กำลัง formalize ทฤษฎี divided powers ใน Lean
- ระหว่างฤดูร้อน Lean เผยให้เห็นปัญหาในเหตุผลแบบมนุษย์ของเอกสารมาตรฐาน และเมื่อตรวจสอบแล้ว lemma สำคัญในงานของ Roby ดูเหมือนจะผิด
- ในเชิงเทคนิค บทความของ Berthelot ไม่ได้พัฒนาทฤษฎี divided powers ตั้งแต่ต้น แต่ใช้ “Les algebres a puissances divisees” ของ Roby
- บทความดังกล่าวตีพิมพ์ใน Bull Sci Math, 2ième série, 89, 1965, หน้า 75-91
- Lemme 8 หน้า p86 ดูเหมือนเป็นเท็จ และยังไม่ชัดเจนว่าจะแก้บทพิสูจน์อย่างไร
- บทพิสูจน์นั้นอ้าง lemma อื่นในบทความ Ann Sci ENS ปี 1963 ของ Roby อย่างผิดพลาด
- ประพจน์ที่ถูกต้องคือ
Gamma_A(M) tensor_A R = Gamma_R(M tensor_A R)แต่ในขั้นตอนการนำไปใช้ มี tensor product ตัวหนึ่งหายไป
- ปัญหานี้ทำให้บทพิสูจน์ของ Roby ที่ว่า divided power algebra ของ module มี divided powers ใช้ไม่ได้ และส่งผลให้ไม่สามารถนิยามวงแหวน
A_crisได้
สถานการณ์ใกล้เคียงกับ “บทพิสูจน์มีช่องว่าง” มากกว่า “ทฤษฎีผิด”
- ไม่ได้หมายความว่า crystalline cohomology เองผิดในทางปฏิบัติ
- ทฤษฎีบทหลัก ๆ ยังดูเหมือนถูกต้อง แต่บทพิสูจน์ที่ Antoine และ Maria Ines กำลังตามอยู่นั้น ไม่สมบูรณ์
- Roby, Grothendieck และ Berthelot ล้วนเสียชีวิตแล้ว จึงไม่สามารถถามผู้เชี่ยวชาญดั้งเดิมได้โดยตรง
- ผู้เชี่ยวชาญหลายคนมองว่าแม้ lemma ระหว่างทางจะเป็นเท็จ แต่บทพิสูจน์ของผลลัพธ์หลักน่าจะแก้ได้
- ในการ formalize แค่การตัดสินว่า “น่าจะแก้ได้” ยังไม่เพียงพอ จำเป็นต้องมีบทพิสูจน์ที่แก้แล้วจริง ๆ
ทางเลี่ยงที่เปิดขึ้นจากภาคผนวกของ Berthelot-Ogus
- Tadashi Tokieda เล่าเรื่องนี้ให้ Brian Conrad ฟังที่ Stanford และ Conrad ถามว่าประเด็นที่ว่า crystalline cohomology ผิดนั้นหมายถึงอะไร
- หลังได้ฟังรายละเอียดทางเทคนิค Conrad เห็นด้วยว่าดูเหมือนมีปัญหา แล้วเริ่มตรวจสอบ
- ไม่กี่ชั่วโมงต่อมา Conrad แจ้งว่าในภาคผนวกของหนังสือ crystalline cohomology ของ Berthelot-Ogus มีบทพิสูจน์อีกแบบว่า universal divided power algebra of a module มี divided powers
- จากมุมมองของ Conrad วิธีนี้ดูใช้ได้ และด้วยเหตุนี้บทพิสูจน์จึงกลับมาเดินหน้าต่อได้
- ต่อมาระหว่างรับประทานอาหารกลางวันกับ Arthur Ogus ที่ Berkeley เมื่อเล่าว่าภาคผนวกนี้ช่วยแก้ปัญหาให้ได้ Ogus ตอบว่าภาคผนวกนั้นก็มีข้อผิดพลาดหลายจุด แต่เขารู้วิธีแก้
เหตุผลที่เอกสารคณิตศาสตร์สมัยใหม่ต้องการการ formalize
- กระบวนการนี้เผยให้เห็นว่าวิธีที่มนุษย์บันทึกคณิตศาสตร์สมัยใหม่อาจยังไม่แข็งแรงพอ
- ข้อเท็จจริงจำนวนมากยังคงอยู่ในสถานะ “ผู้เชี่ยวชาญรู้กันอยู่แล้ว” และอาจไม่ได้ถูกจัดวางไว้อย่างถูกต้องในเอกสาร
- แม้แนวคิดสำคัญจะแข็งแรงพอที่จะทนต่อแรงกระแทกแบบนี้ แต่รายละเอียดบทพิสูจน์จริงอาจไม่ได้อยู่ในตำแหน่งที่คาดไว้
- หากบันทึกคณิตศาสตร์อย่างถูกต้องในระบบ formal จะช่วยลดโอกาสเกิดข้อผิดพลาดได้มาก
- แม้สำหรับนักคณิตศาสตร์ที่ไม่ใช่ formalist หากต้องการให้เครื่องเรียนรู้ข้อโต้แย้งของมนุษย์และทำคณิตศาสตร์ได้เอง ก็จำเป็นต้องมีขั้นตอนสอนข้อโต้แย้งเหล่านั้นให้เครื่องก่อน
- Maria Ines ได้ บรรยาย เกี่ยวกับการ formalize divided powers ใน Cambridge Formalization of Mathematics seminar และเข้าใจว่าปัญหาเหล่านั้นได้รับการจัดการแล้ว
- โปรเจกต์กลับมาเข้าที่เข้าทางอีกครั้ง แต่ก็ยังมีความเป็นไปได้ที่เอกสารอ้างอิงจะกลับมาเป็นอุปสรรคอีก
1 ความคิดเห็น
ความคิดเห็นบน Hacker News
นึกถึงตอนเรียนบัณฑิตศึกษา ที่เคยเขียนโค้ดเร็ว ๆ เพื่อช่วยแนวทางเชิงคำนวณของอาจารย์ที่ปรึกษาต่อ ข้อคาดการณ์ Birch–Swinnerton-Dyer
ในสัมมนาทฤษฎีจำนวนที่เมืองใกล้ ๆ มีคนถามว่า “คุณพยายามเสริมหลักฐานสนับสนุนข้อคาดการณ์นี้ใช่ไหม” ผมจึงยิ้มแล้วตอบว่า “ไม่ครับ ผมอยากหาตัวอย่างโต้แย้งมากกว่า” แล้วผู้เชี่ยวชาญก็โกรธกันมาก
ทฤษฎีจำนวนเก่าแก่และลึกซึ้งมากจนการเขียนวิทยานิพนธ์ปริญญาเอกในสาขานั้นแทบจะเป็นแค่ก้าวแรกของการเป็นมือใหม่ และแม้จะรู้สัญลักษณ์กับนิยาม แต่ก็ยังเข้าไม่ถึงสัญชาตญาณที่อยู่ข้างใต้
ดังนั้นความโกรธที่ผู้เชี่ยวชาญแสดงต่อคำว่า “หวังว่าจะเจอตัวอย่างโต้แย้ง” จึงทำให้เกิดความอยากรู้มากกว่าความกลัว และทำให้สงสัยว่าพวกเขากำลังมองเห็นอะไรอยู่ แม้ยังอธิบายออกมาเป็นคำพูดไม่ได้
ความก้าวหน้าของการทำให้เป็นรูปนัย แบบนี้ทำให้คณิตศาสตร์เข้าถึงได้มากขึ้นมากสำหรับคนที่คุ้นกับการเขียนโปรแกรมมากกว่า
ความกังวลเรื่องความเป็นรูปนัยที่ไม่เพียงพอนั้นชอบธรรม แต่ผมมองว่าปฏิกิริยาที่ถูกต้องต่อความกังวลไม่ใช่การหลีกเลี่ยง แต่คือความอยากรู้
ถ้ามือใหม่หัดเดินอย่างคุณหาตัวอย่างโต้แย้งได้ด้วยการคำนวณหยาบ ๆ แล้วโด่งดังในชั่วข้ามคืน ความพยายามและโครงสร้างทั้งหมดนั้นอาจพังทลาย พวกเขาจึงคงโกรธ
ถ้าจะให้คำแนะนำกับตัวเองสมัยหนุ่ม ๆ ตอนเรียนบัณฑิตศึกษาคณิตศาสตร์ ผมจะบอกว่า สำหรับโจทย์ “จงพิสูจน์ X” ที่ไม่ใช่เรื่องเล็กน้อยทุกข้อ ให้ใช้เวลาอย่างน้อย 1/4 ไปกับ การหาตัวอย่างโต้แย้ง
ในการบ้านอาจล้มเหลว 99% แต่จะได้ความเข้าใจในปัญหามากขึ้นมาก และในอีก 1% ที่เหลือ คุณอาจดูเหมือนอัจฉริยะได้
พอเข้าสู่งานวิจัยคณิตศาสตร์จริง ๆ ความน่าจะเป็นนั้นจะเปลี่ยนไปเข้าข้างแนวทางที่เริ่มจากการหาตัวอย่างโต้แย้งก่อนมากขึ้น
จำได้ว่าตอนเป็นนักศึกษา เพื่อนเล่าให้ฟังว่ามีคนคนหนึ่งเพิ่งจบวันแรกของสัมมนา และทุกคนตื่นเต้นกันว่าเขาจะพิสูจน์ ทฤษฎีบทสุดท้ายของแฟร์มาต์ ได้
คนคนนั้นคือ Andrew Wiles และหลังจากนั้นเขาใช้เวลาอีกหลายเดือนแก้ปัญหาที่พบก่อนตีพิมพ์ จนในที่สุดงานทั้งหมดก็ได้รับการตีพิมพ์
ในฐานะคนที่เรียนคณิตศาสตร์อยู่ มันเป็นเหตุการณ์ที่น่าตื่นเต้นอย่างมหาศาล ดังนั้นพอเห็นคำว่า “บทพิสูจน์ยุค 1990 แบบเก่า” ก็รู้สึกแก่ขึ้นมาจริง ๆ
แทบทั้งชั้นเป็นนักศึกษาบัณฑิตศึกษาคณิตศาสตร์ และผมคิดว่าตัวเองเข้าใจเนื้อหาไม่ถึง 20%
ชอบตอนที่ Lean ทำสิ่งชวนหงุดหงิดแบบที่มันทำเป็นบางครั้ง: มันบ่นกับการนำเสนอข้อโต้แย้งแบบมนุษย์ในวรรณกรรมมาตรฐาน และพอดูละเอียด ๆ แล้วปรากฏว่าข้อโต้แย้งของมนุษย์มีส่วนที่ขาดอยู่จริง
นอกเหนือจากความหงุดหงิดแบบติดตลกแล้ว เรื่องนี้ยอดเยี่ยมมาก และคิดว่า Lean กับเครื่องพิสูจน์ทฤษฎีบทอื่น ๆ จะกลายเป็นเครื่องมือสำคัญในคณิตศาสตร์ต่อไป
ประเด็นที่ว่าเอกสารคณิตศาสตร์สมัยใหม่ทำไว้ไม่ดี ทำให้นึกถึง UI/UX/เว็บดีไซน์
นักออกแบบทำม็อกอัป โปรโตไทป์ และโฟลว์การโต้ตอบที่ไม่เป็นรูปนัยและไม่แม่นยำ แล้วส่งต่อให้นักพัฒนา จากนั้นนักพัฒนาต้องทำให้มันเป็นรูปนัยในโค้ดและอธิบายให้เครื่องเข้าใจอย่างแม่นยำ
ในกระบวนการนั้น ย่อมต้องเจอช่องโหว่อย่างสถานการณ์การโต้ตอบหรือเส้นทางโค้ดที่การออกแบบไม่ได้พิจารณาไว้ และบางครั้งก็เผยให้เห็นข้อบกพร่องใหญ่ในการออกแบบ ซึ่งนักพัฒนาหรือนักออกแบบต้องมาอุดช่องว่างเหล่านั้น
การออกแบบกับการพัฒนาเป็นบทบาทที่ต่างกันและต้องใช้วิธีคิดต่างกัน นักออกแบบส่วนใหญ่จึงต่อต้านอย่างมากต่อการทำงานและคิดแบบนักพัฒนา
หลังความล้มเหลวนั้น เราได้เรียนรู้ว่าเราไม่สามารถทำให้คณิตศาสตร์ทั้งหมดเป็นรูปนัยได้ และนี่ชี้ไปยังปัญหาพื้นฐานของแนวทางที่พยายามใช้ AI ทำคณิตศาสตร์
ถ้าสนใจหัวข้อนี้ ควรดูโค้ดจริง
ตัวอย่าง: https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/M...
พิมพ์เขียวที่อธิบายโครงสร้างทั้งหมดของโค้ดก็น่าดู: https://imperialcollegelondon.github.io/FLT/blueprint/
แม้มองจากคนนอก แต่การได้เห็นว่า โค้ด Lean หน้าตาเป็นอย่างไร และผู้คนมีส่วนร่วมกันอย่างไรนั้นน่าสนใจมาก
อีกอย่างที่ดีคือไม่ต้องมี unit test ในความหมายหนึ่ง ประพจน์พิสูจน์สุดท้ายก็คือ unit test นั่นเอง
เช่น ตัวอย่างเล็ก ๆ และตัวอย่างโต้แย้งที่ใช้ตรวจสอบว่านิยามบางอย่างไม่ว่างเปล่า ก็ทำหน้าที่แบบนั้น
จากมุมมองของคนที่เคยทำคณิตศาสตร์บริสุทธิ์ ปัญหาใหญ่คือ นักคณิตศาสตร์แทบไม่เคยให้บทพิสูจน์ที่สมบูรณ์ในตัวเอง
ไม่มีแรงจูงใจให้ทำแบบนั้น และบางครั้งผู้เขียนก็ภูมิใจกับการ “ละรายละเอียดไว้” ด้วยซ้ำ
สุดท้ายแล้ว หากต้องการบทพิสูจน์ที่เข้มงวดจนตามทุกขั้นตอนทางตรรกะได้ ผู้เชี่ยวชาญก็ต้องมาเติมช่องว่างที่หาได้ไม่ง่ายในเอกสารวิชาการ
บางทีก็จะเป็นไปได้ก็ต่อเมื่อคนแบบนั้นเขียนหนังสืออธิบายทุกอย่าง และบางครั้งแม้เท่านั้นก็ยังไม่พอ
ถ้าดูเฉพาะสิ่งที่ถูกบันทึกไว้ คณิตศาสตร์สมัยใหม่จำนวนมากตั้งอยู่บน รากฐานที่ไม่มั่นคง
บทความวิจัยคณิตศาสตร์เขียนขึ้นเพื่อผู้เชี่ยวชาญคนอื่นในสาขานั้น และบางครั้งรายละเอียดก็น้อยเกินไป จนต้องบ่นเรื่องนี้บ่อย ๆ ในการ peer review
แต่ถ้าให้รายละเอียดทั้งหมดจริง ๆ บทความก็จะยาวขึ้นมาก
ตัวอย่างที่คนมีพื้นฐานคณิตศาสตร์มัธยมปลายแน่น ๆ น่าจะแก้ได้ คือโจทย์ให้พิสูจน์ว่ามีค่าคงที่ C, X > 0 ที่ทำให้สำหรับจำนวนจริง x > X บางตัว มี
log(x^2 + 1) + sqrt(x) + x/exp(sqrt(4x + 3)) < Cxประพจน์รูปแบบนี้พบได้ตลอดในทฤษฎีจำนวนเชิงวิเคราะห์ และสำหรับผู้เชี่ยวชาญแล้วชัดเจนมาก จึงแทบมักเขียนไว้ในบทความโดยไม่มีบทพิสูจน์
หากทำบทพิสูจน์ที่สมบูรณ์และเข้มงวดขึ้นมา ก็จะยาวและน่าเบื่อ และไม่มีผู้เชี่ยวชาญคนไหนอยากอ่าน
ท่าทีแบบนี้มี ต้นทุนจากการประนีประนอม อยู่ แต่ดูเหมือนอยู่ในระดับที่จัดการได้
ฟังดูคล้ายขั้นที่สามที่ Tao พูดถึง คือ สัญชาตญาณที่มีข้อมูลรองรับ
เขาบอกว่า “ถ้าคุณทำอะไรสักอย่างมา 100 ครั้งแล้ว ก็พูดว่า ‘สังเกตได้ง่ายว่า’ แล้วข้ามไปได้”
พูดอีกอย่างคือ ผมเข้าใจว่าต้องมีคนที่มีฐานข้อมูลอยู่ในหัว ทำหน้าที่ค้นหาว่าเงื่อนไขตั้งต้นของทฤษฎีบทใดสักบทกับข้อสรุปของประโยคถัดไปนั้นตรงกันหรือไม่
หรือมีคณิตศาสตร์บางอย่างที่ยังไม่สามารถแสดงออกในรูปแบบที่ proof checker ปัจจุบันประเมินได้กันแน่
หรือไม่อย่างนั้น การใช้ proof checker อาจยังไม่แพร่หลายอย่างที่คิด ฟังดูคล้ายตำแหน่งของ ภาษาแบบ static typing ในวงการโปรแกรมมิง
กล่าวคือ อยากถามว่าเคยมีกรณีที่บทพิสูจน์ซึ่งได้รับการยอมรับอย่างกว้างขวางมีข้อบกพร่องร้ายแรง เพราะส่วนที่ข้ามไปแบบโบกมือผ่าน ๆ หรือเปล่า
ถ้าไม่เคยเกิดเรื่องแบบนั้น ก็พอเข้าใจได้ว่าทำไมจึงมีท่าทีผ่อนคลายต่อการระบุรายละเอียดให้ชัดเจน
ผมสงสัยมาตลอดว่าสัญชาตญาณที่ว่า “crystalline cohomology ถูกใช้กันมากมาตั้งแต่ทศวรรษ 1970 ถ้ามีปัญหาก็น่าจะโผล่มานานแล้ว” นั้นถูกต้องจริงหรือไม่
เป็นไปไม่ได้ถึงขนาดนั้นจริงหรือ ที่คณิตศาสตร์ทั้งสาขาหนึ่งจะถูกพัฒนาขึ้นบนบทพิสูจน์ที่มีข้อบกพร่อง แล้วสาขานั้นกลับกลายเป็นเท็จไปเฉย ๆ
เขาได้เห็นด้วยตัวเองว่าสาขาหนึ่งพังลงเพราะความผิดพลาดใน “เลมมาแรกของหน้าแรก” ของบทความรากฐาน
กระแสที่นำไปสู่งานช่วงต้นเกี่ยวกับ UniMath ปีพิเศษที่ IAS และหนังสือ HoTT อาจกล่าวได้ว่าช่วยผลักดันหัวข้อการทำให้คณิตศาสตร์เป็นรูปแบบทางการมาถึงจุดที่เป็นอยู่ในปัจจุบัน
ถ้ารากฐานผิด ตัวอย่างโต้แย้งหนึ่งในนั้นก็อาจหักล้างทฤษฎีบทพื้นฐานได้ด้วย ดังนั้นการสร้างต่อบนรากฐานที่ผิดกลับมีแนวโน้มจะเปิดเผยข้อบกพร่องของรากฐานมากขึ้น
ในทำนองเดียวกัน เมื่อคณิตศาสตร์ถูกนำไปใช้เป็นครั้งคราวเพื่อสร้างคำทำนาย หากคณิตศาสตร์ผิด คำทำนายก็จะผิดด้วย และคำทำนายที่ผิดนั้นจะดึงดูดความสนใจมาก
ที่จริงคำว่า “สาขา” อาจชวนเข้าใจผิดเล็กน้อย เพราะทฤษฎีจำนวนมากใกล้เคียงกับ ปม ที่ผูกเข้ากับทฤษฎีอื่น ๆ อีกหลายทฤษฎีทั่วทั้งคณิตศาสตร์มากกว่า
แล้วทฤษฎีเหล่านั้นก็เชื่อมต่อกับทฤษฎีอื่น ๆ อีกต่อหนึ่ง
หากรากฐานพังลงในเชิงตรรกะโดยไม่ส่งผลต่อส่วนอื่นใดของปมเลย ก็คงเป็นสถานการณ์ที่แปลกมาก
ก้อนคณิตศาสตร์ลอย ๆ ขนาดใหญ่ที่ภายในสอดคล้องกันอย่างสมบูรณ์ แต่มีข้อผิดพลาดเพียงจุดเดียว เป็นสิ่งที่นึกภาพได้ยากในกรณี cohomology ของบทความนี้
พูดอย่างเคร่งครัด นี่ใกล้เคียงกับท่าทีเชิงปรัชญา แต่ผมอยากเชื่อว่าคณิตศาสตร์จำนวนมากในปัจจุบัน ในความหมายหนึ่ง ถูกค้นพบขึ้นอย่างเป็นธรรมชาติ
สปอยล์ก็คือ ถึงอย่างนั้นโลกก็ยังหมุนต่อไป
ตลอดราวหนึ่งปีที่ผ่านมา ได้ลองเป็นครั้งคราวที่จะ formalize บางส่วนของหลักสูตร complex analysis ระดับปริญญาตรีใน Lean
ได้เรียนรู้อะไรมากและรู้สึกคุ้มค่า แต่บางครั้งก็อึดอัด
เพิ่งไม่นานมานี้เองที่สามารถนิยาม รูปเชิงขั้ว ได้อย่างสมบูรณ์ในฐานะฟังก์ชันหนึ่งต่อหนึ่งทั่วถึงจาก C* ไปยัง (-pi,pi] x R ทั้งที่ complex numbers, power series, exp, sin มีอยู่ใน mathlib แล้ว แต่เป็นเพราะดื้อจะนิยาม “ตั้งแต่ศูนย์”
ความยากส่วนใหญ่อาจเกิดจากมีพื้นฐานแค่ปริญญาตรีคณิตศาสตร์ ไม่คุ้นกับ Lean/mathlib และไม่มีคนคอยแนะนำ อย่างไรก็ดี ชุมชน Zulip ช่วยได้มากจริง ๆ
ผลลัพธ์จำนวนมากใน mathlib ถูกเขียนไว้ค่อนข้างเป็นนามธรรม จึงยากจะเข้าใจว่ามันเชื่อมโยงกับทฤษฎีบทมาตรฐานระดับปริญญาตรีอย่างไร หรือมีทฤษฎีบทแบบนั้นอยู่ใน mathlib หรือไม่
สำหรับชุมชนคณิตศาสตร์วิจัยอาจสมเหตุสมผล แต่สำหรับผมแล้วเป็นอุปสรรคใหญ่ และถ้า Lean ถูกใช้ในการศึกษามากขึ้น ก็น่าจะเกิดปัญหาคล้ายกันได้ อย่างไรก็ดี เป็นเรื่องที่จัดระเบียบได้เมื่อเวลาผ่านไป
มองว่าระบบอัตโนมัติในการพิสูจน์ยังไม่เพียงพอ
หลายอย่างพิสูจน์ยากกว่าที่ควรจะเป็นมาก โดยเฉพาะ การแปลงชนิดข้อมูล เป็นเรื่องที่ไม่พอใจที่สุด
ในคณิตศาสตร์ทั่วไป จำนวนจริงเป็นสับเซตของจำนวนเชิงซ้อน ดังนั้นสิ่งที่เป็นจริงสำหรับจำนวนเชิงซ้อนทั้งหมดก็เป็นจริงสำหรับจำนวนจริงทั้งหมดโดยอัตโนมัติ แต่ใน Lean ทั้งสองเป็นคนละ type และต้องไปมาผ่านฟังก์ชันฉีด/ตัวดำเนินการแปลงชนิดข้อมูล ทำให้แก่นของการพิสูจน์พร่ามัว
เมื่อการแปลงชนิดข้อมูลซ้อนกัน เช่น แปลง natural numbers เป็น real numbers แล้วต่อไปเป็น complex numbers จะยิ่งรกเป็นพิเศษ
แน่นอนว่านี่อาจเป็นปัญหาเฉพาะหัวข้อนี้ และในสาขาอย่าง algebra ที่จัดการกับ mapping อย่างชัดเจน ก็น่าจะรู้สึกเป็นธรรมชาติกว่ามาก
ขอคำแนะนำเรื่องการใช้ mathlib ว่ามีอะไรอยู่บ้าง และอยู่ตรงไหน ทำได้ง่ายมาก
ปัญหาการแปลงชนิดข้อมูลที่ซ้อนหลายชั้น ส่วนใหญ่แก้ได้ด้วย tactic
norm_castแม้ไม่ใช่คำถามเฉพาะเจาะจง แค่พูดถึงผ่าน ๆ หรือถ้าในโค้ดเห็นสไตล์การพิสูจน์ที่ซับซ้อนเกินจำเป็น ก็อาจได้รับคำแนะนำเรื่อง tactic ที่ไม่เคยรู้มาก่อน
ถ้ารู้สึกแค่ว่า formalization ยากเกินไป แต่ไม่รู้ควรใช้เทคนิคอะไร ก็สามารถถามโดยดึง proof ที่ทำอย่างลำบากและยังไม่น่าพอใจออกมาเป็นตัวอย่างโดด ๆ ให้คนอื่นช่วยย่อให้สั้นลง
คำถามแบบนี้มักได้รับการต้อนรับ และทุกคนก็ได้เรียนรู้มาก
เธรดนี้ดูเหมือนจะเกี่ยวกับวิธีเขียนคณิตศาสตร์ให้ดี
เคยอ่าน เขียน สอน ประยุกต์ใช้ และตีพิมพ์คณิตศาสตร์มาหลายสิบปี และได้รับปริญญาเอกด้านคณิตศาสตร์ประยุกต์ด้วย
เป็นความจริงที่งานเขียนคณิตศาสตร์มีปัญหา และคณิตศาสตร์บางส่วนก็เขียนได้แย่มาก
แต่คณิตศาสตร์ที่เขียนได้ค่อนข้างดีก็มีอยู่
อย่างน้อยที่สุด สัญลักษณ์ทุกตัวควรถูกนิยามก่อนใช้ การให้แรงจูงใจก่อนนำเสนอคณิตศาสตร์ก็ช่วยได้ และบางครั้งคำอธิบายเชิงสัญชาตญาณก็มีประโยชน์
การอ่านคณิตศาสตร์ที่เขียนดีอย่างใส่ใจช่วยให้เรียนรู้ การเขียนคณิตศาสตร์ ได้
ตัวอย่างเช่น Finite-Dimensional Vector Spaces ของ Paul R. Halmos, Advanced Calculus ของ R. Creighton Buck, Mathematical Analysis ของ Tom M. Apostol, Real Analysis ของ H. L. Royden, Real and Complex Analysis ของ Walter Rudin, Probability ของ Leo Breiman และ Mathematical Foundations of the Calculus of Probability ของ Jacques Neveu
ผู้เขียนพยายามตรวจสอบ ทฤษฎีบทสุดท้ายของแฟร์มา ตามแนวทางที่พัฒนามาในวรรณกรรม และในกระบวนการนั้นพบว่า lemma ที่ค้ำจุนสาขาย่อยหนึ่งไว้ ไม่เป็นจริงในรูปแบบที่ถูกนำไปใช้
ถึงอย่างนั้น เหตุผลที่ยังเชื่อว่าสาขานั้นโดยรวมยังพอกู้ได้ ก็เพราะเชื่อว่าถ้ามันผิดจริง คงมีใครสักคนพบผลลัพธ์เชิงลบไปแล้ว
ตอนนี้จึงต้องหาสิ่งทดแทนที่เหมาะสมมาค้ำจุนสาขานั้นแทน
ผู้เขียนเป็นคนเขียนได้สนุกทีเดียว แม้จะเข้าใจไม่ถึงครึ่ง แต่ก็อ่านง่าย เป็นประสบการณ์ที่แปลกดี
พบคำดี ๆ สำหรับใช้เมื่อ proof ถูกหักล้างหรือพบข้อบกพร่อง คือ vitiated
ชอบคำนี้เพราะสื่อได้ว่า proof นั้นเสียหายและต้องมี proof ใหม่หรือการซ่อมแซม โดยไม่ค่อยทำให้เข้าใจผิดว่าข้อสรุปถูกพิสูจน์แล้วว่าเป็นเท็จ