โมเดล AI จีนช่วยพิสูจน์กรณีมิติสามของข้อคาดการณ์ Ghys พร้อมใช้ Lean ตรวจสอบคณิตศาสตร์

ปัญหาคณิตศาสตร์ปี 1995 บรรลุหมุดหมายใหม่

ข้อคาดการณ์ทางคณิตศาสตร์ที่เสนอขึ้นในปี 1995 ได้รับการพิสูจน์ครอบคลุมกรณีมิติเชิงซ้อนสาม หลังนักคณิตศาสตร์ร่วมมือกับโมเดล Intern-S2 ของห้องปฏิบัติการ AI เซี่ยงไฮ้ จากนั้นทีมมหาวิทยาลัยปักกิ่งได้แปลงทฤษฎีบทหลักทั้งสี่ข้อในบทความเป็นบทพิสูจน์ที่ตรวจสอบด้วย Lean ซึ่งเป็นระบบคอมพิวเตอร์ที่ออกแบบมาเพื่อตรวจสอบการให้เหตุผลทางคณิตศาสตร์

ห้องปฏิบัติการ AI เซี่ยงไฮ้ประกาศความสำเร็จเมื่อวันที่ 15 ตุลาคม 2026 โดยระบุว่าเป็นผลงานของทีมที่นำโดยตี๋เซิง ซวี ศาสตราจารย์แห่งมหาวิทยาลัยเกรตเบย์และนักวิชาการอาคันตุกะของห้องปฏิบัติการ บทความวิจัยเรื่อง Codimension-one holomorphic Anosov diffeomorphisms ระบุชื่อเจี่ยซง จาง จากสถาบันเทคโนโลยีแห่งราชอาณาจักรสวีเดน (KTH) เป็นผู้เขียนเพียงคนเดียว

ผลลัพธ์นี้คลี่คลายกรณีโคไดเมนชันหนึ่งของข้อคาดการณ์ที่เอเตียน กีส์ นักคณิตศาสตร์ชาวฝรั่งเศสเสนอไว้ รวมถึงกรณีมิติเชิงซ้อนสามด้วย โจทย์นี้ว่าด้วยความสัมพันธ์อันน่าทึ่งระหว่างการเคลื่อนที่กับรูปร่าง กล่าวคือ พื้นที่ที่รองรับการเคลื่อนที่แบบโกลาหลชนิดหนึ่งจำเป็นต้องมีโครงสร้างทางคณิตศาสตร์ที่เป็นระเบียบสูงหรือไม่

Intern-S2 ช่วยพัฒนาแนวคิดและข้อโต้แย้งผ่านการแลกเปลี่ยนกับนักวิจัยซ้ำหลายรอบ จางระบุในคำชี้แจงการใช้ AI ว่าเขาตรวจสอบคณิตศาสตร์ทั้งหมดด้วยตนเอง ความร่วมมือนี้ผสานการสำรวจด้วยเครื่องจักร การใช้ดุลยพินิจของมนุษย์ และกระบวนการตรวจสอบอย่างเป็นทางการที่แยกต่างหาก

ห้องปฏิบัติการระบุว่าความสำเร็จนี้เป็นครั้งแรกที่มีการใช้โมเดล AI ของจีนช่วยแก้ปัญหาคณิตศาสตร์ในระดับนี้ ผลงานที่เป็นรูปธรรมคือทฤษฎีบทการจำแนก พร้อมเอกสารฉบับร่างที่เผยแพร่ต่อสาธารณะและโค้ดการทำให้เป็นทางการที่เปิดเผยต่อสาธารณะ

บทพิสูจน์บอกอะไรเกี่ยวกับการเคลื่อนที่และรูปร่าง

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

ระบบ Anosov มีการยืดและบีบในสัดส่วนที่แน่นอน เมื่อเคลื่อนที่ซ้ำไปเรื่อย ๆ บางทิศทางจะหดตัว ขณะที่ทิศทางอื่นขยายออก จุดเริ่มต้นที่อยู่ใกล้กันอาจแยกห่างอย่างรวดเร็ว ก่อให้เกิดพฤติกรรมแบบโกลาหล แม้กฎที่กำกับทุกขั้นตอนจะมีความแน่นอนก็ตาม

ภาพที่ช่วยให้เข้าใจได้คือกระบวนการซ้ำ ๆ ที่ยืดและพับรูปร่าง ระบบคณิตศาสตร์ที่ศึกษาในที่นี้มีข้อกำหนดเข้มงวดกว่ามาก กล่าวคือ การยืดและหดต้องเป็นไปตามเงื่อนไขที่สม่ำเสมอ และการเคลื่อนที่ต้องรักษาโครงสร้างที่กำหนดโดยพิกัดเชิงซ้อนไว้

กีส์เสนอว่าระบบลักษณะนี้บนแมนิโฟลด์เชิงซ้อนกะทัดรัดควรมีคำอธิบายเชิงพีชคณิตแบบมาตรฐาน แมนิโฟลด์คือปริภูมิที่ดูเรียบง่ายในบริเวณเล็ก ๆ แม้รูปร่างโดยรวมจะซับซ้อน ส่วนความกะทัดรัดเป็นเงื่อนไขทางคณิตศาสตร์ที่ในบริบทนี้ทำให้ปริภูมิไม่แผ่ขยายออกไปอย่างไม่มีที่สิ้นสุด

ทฤษฎีบทของจางระบุว่าโฮโลมอร์ฟิก Anosov diffeomorphism ทุกตัวที่มีโคไดเมนชันหนึ่งบนแมนิโฟลด์เชิงซ้อนกะทัดรัดและเชื่อมโยงกัน จะสมสัณฐานแบบไบโฮโลมอร์ฟิกกับไฮเพอร์โบลิกออโตมอร์ฟิซึมของทอรัสเชิงซ้อน กล่าวอย่างง่ายคือ การเปลี่ยนพิกัดแบบผกผันได้ที่เคารพโครงสร้างเชิงซ้อนจะเปลี่ยนการเคลื่อนที่ให้เป็นการแปลงเชิงพีชคณิตมาตรฐานบนปริภูมิที่เป็นระเบียบมาก

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

เหตุใดขอบเขตที่ระบุไว้อย่างแม่นยำจึงสำคัญ

บทความนี้ศึกษากรณีโคไดเมนชันหนึ่ง สำหรับระบบเหล่านี้ หมายความว่าส่วนที่หดตัวหรือขยายตัวส่วนใดส่วนหนึ่งมีมิติเชิงซ้อนหนึ่ง ทฤษฎีบทครอบคลุมตระกูลระบบที่มีข้อจำกัดนี้โดยทั่วไป และคลี่คลายข้อคาดการณ์ในมิติเชิงซ้อนสาม

ข้อคาดการณ์ที่กีส์เสนอในวงกว้างกว่านั้นครอบคลุมระบบโฮโลมอร์ฟิก Anosov บนแมนิโฟลด์เชิงซ้อนหลายประเภท และอธิบายระบบเหล่านี้ด้วยแบบจำลองเชิงพีชคณิตมาตรฐานบนปริภูมิที่เรียกว่าอินฟรา-นิลแมนิโฟลด์เชิงซ้อน ผลงานของจางให้คำตอบที่มีโครงสร้างตายตัวเป็นพิเศษสำหรับกรณีที่ศึกษา ได้แก่ทอรัสเชิงซ้อนและไฮเพอร์โบลิกออโตมอร์ฟิซึม

สำหรับนักคณิตศาสตร์ที่ทำงานในกรณีนี้ ทฤษฎีบทเปลี่ยนโจทย์จากการระบุปริภูมิและการเคลื่อนที่ที่ยังไม่ทราบ ไปสู่การศึกษากับแบบจำลองมาตรฐาน การเปลี่ยนพิกัดเชื่อมระบบเดิมเข้ากับแบบจำลองดังกล่าว โดยยังคงรักษาเรขาคณิตเชิงซ้อนไว้

ซวีศึกษาปัญหานี้มาหลายปี ก่อนหน้านี้เขาเคยศึกษากรณีมิติสามร่วมกับอาร์ตูร์ อาวีลา อดีตอาจารย์ที่ปรึกษาและผู้ได้รับเหรียญฟิลด์ส ต่อมาซวีและจางได้ผลลัพธ์บางส่วนที่เกี่ยวข้อง ซึ่งตีพิมพ์ในวารสาร Journal of the European Mathematical Society งานชิ้นใหม่นี้ต่อยอดจากการศึกษาคำถามทางคณิตศาสตร์เดียวกันมาอย่างต่อเนื่อง

จากข้อสอบโอลิมปิกสู่ความร่วมมือวิจัย

บทบาทของ Intern-S2 สืบเนื่องจากผลงานก่อนหน้าของ Intern-S1 ในการแข่งขันคณิตศาสตร์โอลิมปิกจีนปี 2025 คณะกรรมการของสมาคมคณิตศาสตร์จีนที่รับผิดชอบการแข่งขันคณิตศาสตร์ระดับมัธยมศึกษาได้จัดการทดสอบ AI ในปีนั้น โดยเชิญโมเดลจีนสามตัวมาแก้โจทย์ภายในเวลาจำกัดเดียวกับผู้เข้าแข่งขันที่เป็นมนุษย์

Intern-S1 ทำได้ 102 คะแนนตามเกณฑ์การให้คะแนนเดียวกัน และได้อันดับหนึ่งในบรรดาโมเดลสามตัวที่เข้าร่วม เกณฑ์เหรียญทองอยู่ที่ 78 คะแนน ทำให้คะแนนของโมเดลสูงกว่าเกณฑ์ 24 คะแนน หรือราว 31 เปอร์เซ็นต์

ซวีมองเห็นศักยภาพในการนำโมเดลตระกูลนี้มาใช้กับคณิตศาสตร์วิจัย ขณะที่ห้องปฏิบัติการ AI เซี่ยงไฮ้ต้องการขยับจากโจทย์แข่งขันไปสู่คำถามที่ยังไม่มีคำตอบ ความร่วมมือเริ่มขึ้นในช่วงต้นปี 2026 และรวมถึงการสร้างระบบซอฟต์แวร์ที่เรียกว่า Harness เพื่อจัดระเบียบการทำงานของโมเดลและการแลกเปลี่ยนกับนักวิจัย

ขั้นตอนหลักมีดังนี้:

• 1995: เอเตียน กีส์เสนอข้อคาดการณ์
• 2025: Intern-S1 ทำได้ 102 คะแนนในการทดสอบ AI ของการแข่งขันคณิตศาสตร์โอลิมปิกจีน
• ต้นปี 2026: ซวีและห้องปฏิบัติการ AI เซี่ยงไฮ้เริ่มความร่วมมือฝึกโมเดล
• มีนาคม 2026: ซวีเป็นนักวิชาการอาคันตุกะของห้องปฏิบัติการ
• สิงหาคม 2026: Intern-S2 เวอร์ชันที่พัฒนาภายในพร้อมระบบสนับสนุน เข้าสู่ขั้นที่ใช้สำรวจคณิตศาสตร์อย่างเข้มข้น
• 29 กันยายน: บทความของจางเผยแพร่บน arXiv ก่อนมีฉบับแก้ไขเมื่อวันที่ 13 ตุลาคม
• 15 ตุลาคม 2026: มีการประกาศความสำเร็จต่อสาธารณะ

นักคณิตศาสตร์ชี้แนะแนวทางให้ AI อย่างไร

การสำรวจปัญหาครั้งแรกของ Intern-S2 สร้างรายงานการอนุมานยาวประมาณ 400 หน้า ซวีเชิญจาง อดีตลูกศิษย์และนักวิจัยหลังปริญญาเอกที่ KTH มาร่วมงานในฐานะนักวิชาการอาคันตุกะ จางติดตามข้อคาดการณ์ของกีส์มาตั้งแต่สมัยศึกษาปริญญาเอก

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

ห้องปฏิบัติการระบุว่ามีการให้เหตุผลต่อเนื่องเจ็ดรอบ ระหว่างกระบวนการ กราฟปัญหาของโมเดลขยายจาก 15 โหนดเป็น 389 โหนด ขณะที่ผลลัพธ์สะสมมีความยาวราวหนึ่งพันหน้าและประกอบด้วยแนวทางที่เสนอหลายสิบแนวทาง

กราฟปัญหาคือแผนผังของงานคณิตศาสตร์ย่อยและความเชื่อมโยงระหว่างงานเหล่านั้น โหนดหนึ่งอาจแทนข้ออ้างขั้นกลาง ขณะที่อีกโหนดแทนผลลัพธ์ที่จำเป็นต่อการพิสูจน์ข้ออ้างนั้น จำนวนโหนดที่เพิ่มขึ้นตามรายงานแสดงให้เห็นว่าระบบแยกปัญหาและสำรวจปัญหาอย่างกว้างขวางเพียงใด

คำชี้แจงการใช้ AI ของจางระบุโดยตรงว่าใครเป็นผู้รับผิดชอบคณิตศาสตร์ในผลงานฉบับสมบูรณ์: Intern-S2 เวอร์ชันภายในช่วยพัฒนาแนวคิดและข้อโต้แย้งผ่านการสนทนาหลายรอบ และเขาตรวจสอบคณิตศาสตร์ด้วยตนเอง นอกจากนี้ บทความยังขอบคุณซวีสำหรับการหารืออย่างต่อเนื่อง

ซอฟต์แวร์สนับสนุนมีส่วนช่วยอย่างไร

ห้องปฏิบัติการ AI เซี่ยงไฮ้จับคู่โมเดลกับซอฟต์แวร์ที่ออกแบบมาเพื่อจัดการห่วงโซ่การให้เหตุผลที่ยาวและข้อเสนอแนะจากมนุษย์ซ้ำหลายรอบ ระบบสามารถแบ่งคำถามยากออกเป็นงานย่อย สำรวจหลายแนวทาง และส่งผลลัพธ์กลับมาให้นักวิจัยประเมิน

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

จากนั้นนักวิจัยนำประสบการณ์จากระบบสนับสนุนไปปรับปรุงตัวโมเดล เป้าหมายในทางปฏิบัติคือทำให้การทำงานคืบหน้าได้อย่างเป็นประโยชน์ตลอดการศึกษาที่ยาวนาน รวมถึงติดตามผลลัพธ์ระหว่างทางและแก้ไขข้อผิดพลาดเมื่อมีข้อโต้แย้งใหม่เกิดขึ้น

ห้องปฏิบัติการยังอ้างถึงผลการทดสอบบน IMO-Proof และ AdvancedMathBench ซึ่งเป็นการประเมินที่มุ่งวัดการให้เหตุผลทางคณิตศาสตร์ สำหรับโครงการข้อคาดการณ์ของกีส์ หลักฐานโดยละเอียดที่สุดเกี่ยวกับการทำงานของระบบคือชุดการอนุมานขนาดใหญ่ ข้อเสนอแนะจากผู้เชี่ยวชาญ บทความที่เสร็จสมบูรณ์ และการตรวจสอบอย่างเป็นทางการในขั้นต่อมา

มหาวิทยาลัยปักกิ่งตรวจสอบบทพิสูจน์อย่างไร

ทีมมหาวิทยาลัยปักกิ่งนำโดยปิน ตงและรั่วชวน หลิว ใช้กรอบการทำงาน SHEAF เพื่อทำให้ทฤษฎีบทหลักทั้งสี่ข้อในบทความของจางเป็นทางการ งานนี้ยังครอบคลุมผลลัพธ์ของกีส์ที่ใช้เป็นฐานของข้อโต้แย้งด้วย

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

เจี่ยตง เจียงและปิน อู๋ สมาชิกทีมระบุว่าการดำเนินงานใช้เวลาราวห้าวัน โดยมี AI agent ทำงานพร้อมกันสูงสุด 100 ตัว และสร้างโค้ด Lean ราว 550,000 บรรทัด ผู้เชี่ยวชาญยังตรวจสอบด้วยว่าข้อความที่เขียนอย่างเป็นทางการตรงกับความหมายทางคณิตศาสตร์ของทฤษฎีบทหลักในบทความ

SHEAF จัดงานเป็นกราฟมีทิศทางของนิยาม ข้อเสนอ และความเชื่อมโยงระหว่างกัน จึงทำให้ agent หลายตัวทำงานกับส่วนที่เชื่อมโยงกันได้ ขณะที่ทีมติดตามว่าข้อความใดมีบทพิสูจน์แล้วและข้อใดยังต้องดำเนินการ

การทำให้เป็นทางการต้องทำมากกว่าการแปลงข้อโต้แย้งขั้นสุดท้าย ผลลัพธ์สนับสนุนบางส่วนในสาขาพลวัตยังไม่มีอยู่ในคลังคณิตศาสตร์แบบเป็นทางการที่มีอยู่ ทีมจึงต้องวางรากฐานดังกล่าวขึ้นมา หรือหาแนวทางที่ใช้ผลลัพธ์ที่มีอยู่แล้ว ก่อนเชื่อมส่วนต่าง ๆ ให้เป็นห่วงโซ่ที่สมบูรณ์

บทความเผยแพร่ในรูปเอกสารฉบับร่างบน arXiv และโค้ดการทำให้เป็นทางการเผยแพร่บน GitHub ประกาศดังกล่าวไม่ได้ระบุว่าบทความได้รับการตีพิมพ์ในวารสารหรือผ่านการพิจารณาโดยผู้ทรงคุณวุฒิแล้วหรือไม่

เหตุใดทั้งสองขั้นตอนจึงต้องดำเนินควบคู่กัน

Intern-S2 และ SHEAF ทำหน้าที่ต่างกัน ระบบแรกช่วยค้นหาแนวคิดและข้อโต้แย้งทางคณิตศาสตร์ ส่วนระบบที่สองช่วยสร้างบทพิสูจน์อย่างเป็นทางการที่ Lean ตรวจสอบได้ นักคณิตศาสตร์ที่เป็นมนุษย์ชี้นำการสำรวจ ตรวจสอบคณิตศาสตร์ที่ได้ และประเมินว่าข้อความที่ทำให้เป็นทางการถ่ายทอดทฤษฎีบทตามที่ตั้งใจไว้หรือไม่

ขนาดของงานทำให้การแบ่งหน้าที่นี้เห็นได้ชัด ผลลัพธ์จากการสำรวจราวหนึ่งพันหน้าถูกนำไปใช้จัดทำบทความวิจัย จากนั้นกระบวนการตรวจสอบสร้างโค้ดอย่างเป็นทางการราว 550,000 บรรทัด แต่ละขั้นแปลงงานให้อยู่ในรูปแบบที่เหมาะกับภารกิจต่างกัน

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

ขั้นต่อไปคือโมดูลตรวจสอบที่นำกลับมาใช้ได้

ห้องปฏิบัติการ AI เซี่ยงไฮ้วางแผนบรรจุกระบวนการทำงานนี้เป็นโมดูลตรวจสอบทางคณิตศาสตร์สำหรับแพลตฟอร์มค้นพบทางวิทยาศาสตร์ Intern Duanyan เป้าหมายคือให้โครงการในอนาคตนำการผสานการสำรวจด้วยโมเดล ข้อเสนอแนะจากผู้เชี่ยวชาญ และการตรวจสอบอย่างเป็นทางการไปใช้ซ้ำได้

ห้องปฏิบัติการยังตั้งใจนำความสามารถด้านการให้เหตุผลที่พัฒนาขึ้นจากโครงการนี้ไปใช้กับสาขาอื่นที่มีโครงสร้างทางคณิตศาสตร์คล้ายกัน วงจรที่เสนอคือแก้ปัญหาวิจัย นำวิธีที่เป็นประโยชน์มาพัฒนาเป็นซอฟต์แวร์ที่ใช้ซ้ำได้ แล้วนำไปใช้กับการศึกษาเรื่องอื่น

สำหรับซวี ผลงานนี้ต่อยอดความสนใจด้านการวิจัยที่สั่งสมมายาวนานผ่านความร่วมมือระหว่างมหาวิทยาลัยเกรตเบย์ ห้องปฏิบัติการ AI เซี่ยงไฮ้ KTH และมหาวิทยาลัยปักกิ่ง สำหรับวงการคณิตศาสตร์ในวงกว้าง ผลงานนี้นำเสนอทั้งผลการจำแนกแบบใหม่และตัวอย่างโดยละเอียดของการมีส่วนร่วมของ AI ในงานวิจัยภายใต้การชี้นำของมนุษย์

ประเด็นสำคัญ

• บทพิสูจน์ใหม่นี้คลี่คลายกรณีโคไดเมนชันหนึ่งของข้อคาดการณ์ Ghys รวมถึงมิติเชิงซ้อนสาม
• เจี่ยซง จางเป็นผู้เขียนบทความวิจัยเพียงคนเดียว และระบุว่าเขาตรวจสอบคณิตศาสตร์ทั้งหมดด้วยตนเอง
• ตี๋เซิง ซวีและจางชี้แนะแนวทางให้ Intern-S2 ผ่านการสำรวจและให้ข้อเสนอแนะซ้ำหลายรอบ
• กราฟปัญหาของโมเดลขยายจาก 15 โหนดเป็น 389 โหนด พร้อมผลการอนุมานราวหนึ่งพันหน้า
• กรอบการทำงาน SHEAF ของมหาวิทยาลัยปักกิ่งช่วยทำให้ทฤษฎีบทหลักสี่ข้อและผลลัพธ์สนับสนุนเป็นทางการใน Lean
• มีรายงานว่ากระบวนการตรวจสอบใช้เวลาราวห้าวันและสร้างโค้ดประมาณ 550,000 บรรทัด
• ห้องปฏิบัติการวางแผนพัฒนากระบวนการนี้เป็นโมดูลตรวจสอบทางคณิตศาสตร์ที่นำกลับมาใช้ได้