ที่มา: ชุมชนทัวริง

ผู้แต่ง: Lin Jun Cen Feng

Wu Wenjun ในที่ทำงาน (12 พฤษภาคม 1919-7 พฤษภาคม 2017) ที่มา: Academy of Mathematics and Systems Science, Chinese Academy of Sciences

ปี 1979 เป็นปีที่สำคัญของจีน เหตุการณ์สำคัญหลายเหตุการณ์เกิดขึ้นในปีนี้ และยังถือเป็นจุดเปลี่ยนที่สำคัญในด้านการเมือง เศรษฐกิจ วิทยาศาสตร์และเทคโนโลยี วัฒนธรรม และสาขาอื่นๆ ของจีน และเป็นหนึ่งในจุดหักเหของช่วงเวลาที่สำคัญในประวัติศาสตร์จีนสมัยใหม่ เมื่อเทียบกับยุคใหม่อันงดงามที่เปิดในปี 1979 การเริ่มต้นการวิจัยปัญญาประดิษฐ์ (AI) ในประเทศจีนในปี 1979 ถือได้ว่าเป็นคลื่นที่ไม่โดดเด่นในกระแสประวัติศาสตร์ แต่ในประวัติศาสตร์ของปัญญาประดิษฐ์ในประเทศจีน นี่เป็นการก้าวล้ำ เหตุการณ์.

โรงเรียนปัญญาประดิษฐ์ยุคแรกสุดคือโรงเรียนแห่งสัญลักษณ์ นักวิทยาศาสตร์ปัญญาประดิษฐ์ยุคแรกสุดส่วนใหญ่เป็นนักคณิตศาสตร์และนักตรรกศาสตร์ พวกเขารวมคอมพิวเตอร์เข้ากับงานวิจัยของตนเองหลังจากกำเนิดคอมพิวเตอร์ จึงเข้าสู่สาขาปัญญาประดิษฐ์ ในประเทศจีนก็เป็นนักคณิตศาสตร์เช่นกันที่เปิดหน้าแรกของการวิจัยปัญญาประดิษฐ์ ในปี 1979 ไม่ว่าจะเป็น "Wu Method" ในการพิสูจน์ด้วยเครื่องจักรที่เผยแพร่ไปทั่วโลก หรือการจัดการประชุม Computer Science Summer Symposium ที่เทียบได้กับการประชุม Dartmouth Conference ก็มีนักคณิตศาสตร์อยู่เบื้องหลัง ในปีนี้เองที่ปัญญาประดิษฐ์ของจีนเริ่มตามทันโลก

ผู้เสนอ "Wu Method" ไม่ใช่ใครอื่นนอกจากนักคณิตศาสตร์ Wu Wenjun ร่วมกับ Wang Xianghao และ Zeng Xianchang เขาได้รับการขนานนามว่าเป็น "สามปรมาจารย์แห่งเครื่องพิสูจน์" ในช่วงปลายทศวรรษ 1970 อู๋ เหวินจุน ซึ่งมีอายุเกือบ 60 ปี ได้เริ่มต้นจากการศึกษาคณิตศาสตร์ของจีนโบราณและสร้างสาขาใหม่เกี่ยวกับกลศาสตร์ทางคณิตศาสตร์ เขาเสนอ "วิธีหวู่" สำหรับการพิสูจน์ทฤษฎีบทเรขาคณิตด้วยคอมพิวเตอร์ซึ่งถือเป็น งานบุกเบิกในด้านการใช้เหตุผลอัตโนมัติ

1. Wu Wenjun เปิดประตูให้ปัญญาประดิษฐ์ของจีนก้าวสู่โลก

ในเดือนมกราคม พ.ศ. 2522 ตามคำเชิญของสถาบันเพื่อการศึกษาขั้นสูงในพรินซ์ตัน นักคณิตศาสตร์อู๋ เหวินจุน ได้ขึ้นเที่ยวบินแลกเปลี่ยนไปยังสหรัฐอเมริกาพร้อมกับเงิน 25,000 ดอลลาร์ในกระเป๋าของเขา

เขามาพร้อมกับนักคณิตศาสตร์ Chen Jingrun ทั้งสองเป็นนักวิทยาศาสตร์กลุ่มแรกที่ได้รับเชิญให้ไปศึกษาและเยือนสหรัฐอเมริกาหลังการสถาปนาความสัมพันธ์ทางการทูตระหว่างจีนและสหรัฐฯ พวกเขาจะศึกษา และแลกเปลี่ยนที่สถาบันเพื่อการศึกษาขั้นสูงในพรินซ์ตันเป็นระยะเวลาหนึ่ง หัวข้อการแลกเปลี่ยนของ Chen Jingrun เป็นธรรมชาติ "1+2" และเนื้อหาหลักของการแลกเปลี่ยนของ Wu Wenjun ในการเดินทางครั้งนี้ นอกเหนือจากอาชีพโทโพโลยีเก่าของเขาแล้ว ยังเกี่ยวกับประวัติของคณิตศาสตร์จีนโบราณและกลไกทางคณิตศาสตร์อีกด้วย เขาต้องการ เพื่อใช้เงิน 25,000 หยวน เขานำเงินดอลล่าร์ไปซื้อคอมพิวเตอร์สำหรับการศึกษาเกี่ยวกับกลไกทางคณิตศาสตร์

เมื่อ Wu Wenjun ได้รับรางวัลชนะเลิศสาขาวิทยาศาสตร์ธรรมชาติจาก Chinese Academy of Sciences (ต่อไปนี้จะเรียกว่า "Chinese Academy of Sciences") ในปี 1979 เครื่องจักรทางคณิตศาสตร์ได้กลายเป็นแนวทางการวิจัยหลักของเขา ทิศทางการวิจัยนี้ยังดึงดูดความสนใจของโลก วิธีการวิจัยของ Wu Wenjun เรียกว่า "Wu Method" ในด้านการพิสูจน์ทฤษฎีบทเครื่องจักร รางวัลสูงสุดด้านวิทยาศาสตร์และเทคโนโลยีอัจฉริยะของจีน "Wu Wenjun Artificial Intelligence Science and Technology Award" ใช้ ชื่อของ Wu Wenjun เพื่อระลึกถึง Wu Wenjun ในฐานะความสำเร็จของนักวิจัยชาวจีนในสาขาที่เกี่ยวข้องกับ AI

โดยไม่ได้ตั้งใจ Wu Wenjun ได้เปิดประตูให้การวิจัยปัญญาประดิษฐ์ของจีนก้าวไปสู่ระดับโลก การวิจัยของ Wu Wenjun เกี่ยวกับประวัติศาสตร์คณิตศาสตร์จีนโบราณเริ่มขึ้นในราวปี 1974 ในเวลานั้น Guan Zhaozhi รองผู้อำนวยการสถาบันคณิตศาสตร์แห่ง Chinese Academy of Sciences (ต่อไปนี้เรียกว่า "สถาบันคณิตศาสตร์แห่ง Chinese Academy of Sciences") ขอให้ Wu Wenjun ศึกษาคณิตศาสตร์จีนโบราณ Wu Wenjun ได้ค้นพบความแตกต่างที่สำคัญอย่างรวดเร็วระหว่างประเพณีทางคณิตศาสตร์ของจีนโบราณและประเพณีทางคณิตศาสตร์ของตะวันตกสมัยใหม่ที่สืบทอดมาจากกรีกโบราณ เขาได้ทำการวิเคราะห์อย่างละเอียดเกี่ยวกับการคำนวณทางคณิตศาสตร์ของจีนโบราณ และพัฒนาข้อมูลเชิงลึกที่ไม่เหมือนใครในหลายแง่มุม

ในทศวรรษที่ 1970 การแลกเปลี่ยนทางวิชาการต่างประเทศเริ่มฟื้นตัวอย่างค่อยเป็นค่อยไป ในปี พ.ศ. 2518 อู๋ เหวินจุนเดินทางไปฝรั่งเศสเพื่อแลกเปลี่ยนและเสนอรายงานเกี่ยวกับความคิดทางคณิตศาสตร์ของจีนโบราณที่สถาบันวิทยาศาสตร์ขั้นสูงของฝรั่งเศส ในเวลานี้ Wu Wenjun ได้คืนค่าการพิสูจน์สูตรโบราณของ Rigao และสังเกตเห็นลักษณะ "โครงสร้าง" และ "กลไก" ของคณิตศาสตร์จีนโบราณ ในเทศกาลฤดูใบไม้ผลิปี 1977 อู๋ เหวินจุนได้ตรวจสอบความเป็นไปได้ของวิธีการพิสูจน์ทฤษฎีบทเรขาคณิตด้วยการคำนวณด้วยมือ และกระบวนการนี้ใช้เวลาสองเดือน

แนวคิดดั้งเดิมของการพิสูจน์ทฤษฎีบทของเครื่องจักรมาจากนักให้เหตุผลทางแคลคูลัสของกอตต์ฟรีด วิลเฮล์ม ไลบ์นิซ และต่อมาก็พัฒนามาจากตรรกศาสตร์เชิงสัญลักษณ์ ต่อมา David Hilbert (David Hilbert) ได้เปิดตัว "Hilbert Project" ในปี 1920 บนพื้นฐานนี้ โดยหวังว่าจะทำให้ระบบคณิตศาสตร์ทั้งหมดเป็นจริงอย่างเคร่งครัด พูดง่ายๆ ก็คือ ถ้าแผนนี้เป็นจริง ก็หมายความว่าสำหรับการคาดเดาทางคณิตศาสตร์ใดๆ ก็ตาม ไม่ว่ามันจะยากเพียงใด เราสามารถรู้ได้เสมอว่าการคาดเดานั้นถูกต้อง และพิสูจน์หรือปฏิเสธได้ นี่คือสิ่งที่ฮิลแบร์ตหมายถึงเมื่อเขาพูดว่า "Wir müssen wissen, wir werden wissen" (เราต้องรู้ เราต้องรู้)

อย่างไรก็ตาม หลังจากนั้นไม่นาน ในปี พ.ศ. 2474 เคิร์ต โกเดลได้เสนอทฤษฎีบทความไม่สมบูรณ์ของเกอเดล ซึ่งทำลายอุดมคติของลัทธิพิธีการของฮิลแบร์ต แต่อย่างไรก็ตาม เมื่อโกเดลปิดประตู เขาก็ยังเหลือหน้าต่างไว้ วิทยานิพนธ์ระดับปริญญาเอกของนักคณิตศาสตร์อัจฉริยะชาวฝรั่งเศส Jacques Herbrand ได้วางรากฐานสำหรับทฤษฎีการพิสูจน์และทฤษฎีการเรียกซ้ำของตรรกะทางคณิตศาสตร์ หลังจากเสนอทฤษฎีบทความไม่สมบูรณ์ของ Godel แล้ว Herbrand ได้ตรวจสอบวิทยานิพนธ์ของเขาและทิ้งท้ายไว้ว่า - Gödel และผลลัพธ์ของฉันไม่ขัดแย้งกัน และฉัน เขียนจดหมายถึงโกเดลเพื่อขอคำแนะนำ Gödelตอบ Erblan แต่ Erblan ไม่ได้รอจดหมาย เขาเสียชีวิตในอุบัติเหตุบนภูเขาสองวันหลังจาก Gödel ตอบตอนอายุ 23 ปี ต่อมา รางวัลสูงสุดในสาขาการพิสูจน์ทฤษฎีบทได้รับการตั้งชื่อตามเอล บราวน์ และอู๋ เหวินจุนได้รับรางวัลเอล บราวน์ครั้งที่สี่สำหรับความสำเร็จดีเด่นในการให้เหตุผลอัตโนมัติในปี 1997

นักคณิตศาสตร์คนอื่นๆ ได้เสริมทฤษฎีบทของโกเดล ไม่นานหลังจากที่ Gödel พิสูจน์ว่า "จำนวนเต็มอันดับหนึ่ง (เลขคณิต) ไม่สามารถตัดสินใจได้" Alfred Tarski ได้พิสูจน์ว่า "จำนวนจริงอันดับหนึ่ง (เรขาคณิตและพีชคณิต) สามารถตัดสินใจได้" ซึ่งยังเป็นการวางรากฐานสำหรับการพิสูจน์เครื่องจักรอีกด้วย

ในปี พ.ศ. 2479 ทัวริงได้เขียนบทความสำคัญของเขาเรื่อง "On Computable Numbers, with an Application to the Entscheidungsproblem" (On Computable Numbers, with an Application to the Entscheidungsproblem) ของ Gödel's 1931 ในการพิสูจน์และจำกัดการคำนวณ ผลที่ตามมาก็คือการอภิปรายได้ถูกปรับปรุงใหม่ และภาษาทางการของ Gödel ที่ใช้เลขคณิตทั่วไปถูกแทนที่ด้วยรูปแบบนามธรรมที่เรียบง่ายซึ่งปัจจุบันเรียกว่าเครื่องจักรทัวริง และได้รับการพิสูจน์แล้วว่ากระบวนการที่คำนวณได้ทั้งหมดสามารถจำลองได้ด้วยเครื่องจักรทัวริง นี่เป็นพื้นฐานทางทฤษฎีที่สำคัญสำหรับวิทยาการคอมพิวเตอร์และปัญญาประดิษฐ์ โรงเรียนปัญญาประดิษฐ์ที่เก่าแก่ที่สุด - โรงเรียนสัญลักษณ์ยังขยายออกไปบนพื้นฐานของการดำเนินการทางตรรกะอย่างเป็นทางการ

ย้อนกลับไปที่ Wu Wenjun เขาทำงานในโรงงาน Beijing Radio No. 1 ที่ผลิตคอมพิวเตอร์ในปี 1970 และในเวลานั้นเขาเริ่มติดต่อกับคอมพิวเตอร์และเครื่องพิสูจน์ทฤษฎีบท "วิธีใช้ประโยชน์จากพลังของคอมพิวเตอร์อย่างเต็มที่และนำไปใช้กับงานวิจัยทางคณิตศาสตร์ของเขาเอง" กลายเป็นสิ่งที่อู๋ เหวินจุนสนใจ ต่อมา อู๋ เหวินจุน เริ่มศึกษาประวัติศาสตร์ของคณิตศาสตร์จีนโบราณ และสรุปแนวโน้มพีชคณิตเชิงเรขาคณิตและการคิดอัลกอริทึมของคณิตศาสตร์จีนโบราณ หลังจากค้นพบวิธีคิดที่แตกต่างกันระหว่างคณิตศาสตร์จีนโบราณกับคณิตศาสตร์ตะวันตก เขาตัดสินใจใช้วิธีอื่นในการพิสูจน์ทฤษฎีบทเรขาคณิตด้วยเครื่อง

ในเวลานั้น Wu Wenjun อ่านบทความต่างประเทศมากมายและเข้าใจการพิสูจน์เครื่องจักรอย่างถ่องแท้ ในเวลานั้น งานวิจัยที่ทันสมัยที่สุดเกี่ยวกับการพิสูจน์ทฤษฎีบทของเครื่องจักรมาจากนักตรรกะทางคณิตศาสตร์ Wang Hao ในระหว่างที่เขาศึกษาในภาควิชาคณิตศาสตร์ของ Southwestern Associated University เขาได้ศึกษาภายใต้นักปรัชญาที่มีชื่อเสียงและ "บุคคลแรกในปรัชญาจีน" Jin Yuelin จากนั้นไปมหาวิทยาลัยฮาร์วาร์ดในสหรัฐอเมริกา Willard von Quinn นักปรัชญาและนักตรรกะที่มีชื่อเสียง (W.V. Quinn) ศึกษาระบบสัจพจน์อย่างเป็นทางการที่ก่อตั้งโดย Quine และได้รับปริญญาเอก ในช่วงต้นปี 1953 Wang Hao ได้เริ่มคิดถึงความเป็นไปได้ในการพิสูจน์ทฤษฎีบททางคณิตศาสตร์ด้วยเครื่องจักร

ในปี 1958 Wang Hao ใช้โปรแกรมตรรกะเชิงประพจน์บนคอมพิวเตอร์ IBM 7041 เพื่อพิสูจน์ทฤษฎีบทตรรกศาสตร์อันดับหนึ่งทั้งหมดใน "หลักการคณิตศาสตร์" และพิสูจน์ทฤษฎีบทตรรกศาสตร์เชิงประพจน์ทั้ง 200 รายการเสร็จในปีต่อมา ความสำคัญของงานของ Wang Haozhi อยู่ที่การประกาศความเป็นไปได้ของการใช้คอมพิวเตอร์เพื่อพิสูจน์ทฤษฎีบท เมื่อเขากลับมาที่ประเทศจีนในปี 1977 เขาได้เข้าร่วมในการประชุมสัมมนาหลายครั้งที่ส่งผลต่อการพัฒนาระยะยาวของวิทยาศาสตร์และเทคโนโลยีในประเทศของฉัน และบรรยายพิเศษ 6 ครั้งที่ Chinese Academy of Sciences ซึ่งมีผลกระทบอย่างมากต่อการวิจัยพิสูจน์เครื่องจักรในประเทศ

ใกล้บ้าน ยังมีช่องว่างระหว่างการพิสูจน์ทฤษฎีบทตรรกเชิงประพจน์ของ Wang Hao ใน "หลักการคณิตศาสตร์" ก่อนหน้าของ Wang Hao และการพิสูจน์ทฤษฎีบททางเรขาคณิตที่ Wu Wenjun ต้องการบรรลุ ข้อแรกมีองค์ประกอบตรรกะเชิงสัญลักษณ์มากกว่าในขณะที่อย่างหลังมี องค์ประกอบเหตุผล.. ในเวลานั้น มีงานวิจัยมากมายในต่างประเทศเกี่ยวกับเครื่องพิสูจน์ทฤษฎีบทเรขาคณิต แต่ทั้งหมดก็จบลงด้วยความล้มเหลว

ประการที่สอง จากกลไกทางความคิดทางคณิตศาสตร์ของจีนโบราณสู่ "วิธีวู"

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

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

คณิตศาสตร์จีนโบราณและคณิตศาสตร์สมัยใหม่ของตะวันตกเป็นสองระบบที่แตกต่างกัน อู๋ เหวินจุน ได้ฟื้นฟู "โจวปี้สวนจิง" ตามความรู้และวิธีคิดตามจารีตประเพณีและการให้เหตุผลของคนโบราณในเวลานั้น โดยไม่ใช้ "เครื่องมือสมัยใหม่" เช่น ฟังก์ชันตรีโกณมิติ แคลคูลัส การแยกตัวประกอบ และการแก้สมการลำดับสูงในคณิตศาสตร์สมัยใหม่ วิธีการพิสูจน์ของ "Rigao Tushuo", "Dayanqiuyishu" และ "Zengchengkaifangshu" ใน "Nine Chapters of Shushu" เขาเชื่อว่าคณิตศาสตร์จีนโบราณมีคุณลักษณะเฉพาะของตัวเอง วิธีการของ Qin Jiushao มีลักษณะเฉพาะของการสร้างและการใช้เครื่องจักรกลและสามารถหาผลเฉลยของสมการเชิงพีชคณิตลำดับสูงได้ด้วยเครื่องคิดเลขขนาดเล็ก ในกรณีที่ไม่มีอุปกรณ์คอมพิวเตอร์ประสิทธิภาพสูงในเวลานั้น Wu Wenjun ก็สามารถใช้แนวคิดทางคณิตศาสตร์ของจีนโบราณได้อย่างเต็มที่เพื่อทำการวิจัยเกี่ยวกับการลดขนาด ซึ่งก็น่ายกย่องเช่นกัน

ทฤษฎีบทแรกที่ Wu Wenjun พิสูจน์ตามแนวคิดนี้คือทฤษฎีบทของ Feuerbach ซึ่งพิสูจน์ว่า "วงกลมเก้าจุดของสามเหลี่ยมสัมผัสกับวงกลมที่จารึกไว้และวงกลมที่ล้อมรอบสามวง" นี่เป็นหนึ่งในทฤษฎีบทที่สวยงามที่สุดในเรขาคณิตระนาบ ซึ่งสามารถเห็นได้จากสุนทรียศาสตร์ของ Wu Wenjun ตอนนั้นยังไม่มีคอมพิวเตอร์ ดังนั้น Wu Wenjun จึงคำนวณด้วยมือ ลักษณะเฉพาะอย่างหนึ่งของ "Wu's method" คือจะมีการสร้างพหุนามจำนวนมาก พหุนามที่ใหญ่ที่สุดที่เกี่ยวข้องกับกระบวนการพิสูจน์มีหลายร้อยรายการ การคำนวณนี้ยากมาก และข้อผิดพลาดในขั้นตอนใดขั้นตอนหนึ่งจะทำให้การคำนวณตามมา ล้มเหลว. ในเทศกาลฤดูใบไม้ผลิปี 1977 Wu Wenjun ประสบความสำเร็จในการตรวจสอบวิธีการพิสูจน์ทฤษฎีบทเรขาคณิตด้วยการคำนวณด้วยมือเป็นครั้งแรก ต่อมา Wu Wenjun ได้พิสูจน์ทฤษฎีบทของ Simson บนกำแพงเมืองจีน 203 ที่ผลิตโดย Beijing Radio No. 1 Factory

Wu Wenjun เผยแพร่บทความวิจัยที่เกี่ยวข้อง "ปัญหาการกำหนดเรขาคณิตเบื้องต้นและหลักฐานยานยนต์" ใน "วิทยาศาสตร์จีน" ในปี 1977 และส่งบทความไปยัง Wang Hao Wang Hao พูดถึงงานของ Wu Wenjun อย่างสูง และเขียนตอบกลับเพื่อแนะนำให้ Wu Wenjun ใช้แพ็คเกจพีชคณิตที่มีอยู่และพิจารณาการนำวิธีการของ Wu ไปใช้กับคอมพิวเตอร์ วังห่าวไม่ได้ตระหนักถึงความแตกต่างระหว่างคอมพิวเตอร์ที่ใช้โดยนักวิชาการชั้นนำของจีนและสหรัฐอเมริกาในเวลานี้: กำแพงเมืองจีน 203 สามารถใช้ภาษาเครื่องได้ แต่ระบบคำสั่งของคอมพิวเตอร์ที่แตกต่างกันไม่เป็นสากล และไม่สามารถทำได้ เพื่อใช้แพ็คเกจพีชคณิตที่มีอยู่ ดังนั้น ต่อมา Wu Wenjun เพียงแค่ยืมเครื่องคิดเลขขนาดเล็กจากสถาบันคณิตศาสตร์แห่ง Chinese Academy of Sciences เพื่อเป็นของขวัญจากชาวต่างชาติที่มาเยี่ยมชมสถาบันคณิตศาสตร์แห่ง Chinese Academy of Sciences โดยแปลงประพจน์ให้เป็นรูปแบบพีชคณิต จากนั้นจึงใช้วิธีของ Qin Jiushao เพื่อคำนวณสมการลำดับที่สูงกว่า ปลดเปลื้อง

งานวิจัยของ Wu Wenjun เกี่ยวกับเครื่องพิสูจน์ทฤษฎีบทเรขาคณิตได้รับการสนับสนุนอย่างมากจาก Guan Zhaozhi Guan Zhaozhi เคยศึกษาในฝรั่งเศสและเป็นหนึ่งในผู้ก่อตั้งสมาคมนักวิทยาศาสตร์จีน สาขาฝรั่งเศส เขาได้รวบรวมกลุ่มปัญญาชนผู้รักชาติที่โดดเด่น และ Wu Wenjun ก็เป็นหนึ่งในนั้น ในเวลานั้น สถาบันคณิตศาสตร์ของ Chinese Academy of Sciences ที่ Wu Wenjun ทำงานอยู่มีความสัมพันธ์ที่ซับซ้อน ฝ่ายหนึ่งเชื่อว่าการทำเครื่องพิสูจน์นั้น "ดื้อรั้น" และหวังว่าเขาจะมีส่วนร่วมในการวิจัยโทโพโลยีต่อไป Guan Zhaozhi ผู้ซึ่ง ได้ย้ายจากโทโพโลยีและการวิเคราะห์เชิงฟังก์ชันไปยังทฤษฎีการควบคุมสนับสนุนและเข้าใจเขาเป็นพิเศษ สมมติว่า Wu Wenjun สามารถทำอะไรก็ได้ที่เขาต้องการ ต่อมาเมื่อ Guan Zhaozhi ก่อตั้ง Institute of Systems Science of the Chinese Academy of Sciences ในปี 1979 Wu Wenjun ก็ติดตาม Guan Zhao ไปที่ Institute of Systems Science of the Chinese Academy of Sciences (รูปที่ 1-1)

รูปที่ 1-1 อาคารสำนักงานเดิมของ Institute of Systems Science, Chinese Academy of Sciences (ปัจจุบันคืออาคาร Rongke) ในช่วงต้นทศวรรษ 1980 (จากซ้าย: Xu Guozhi, Wu Wenjun, นักวิชาการชาวอินเดีย, Guan Zhaozhi)

เพื่อพิสูจน์ทฤษฎีบทที่ซับซ้อนยิ่งขึ้น จำเป็นต้องมีเครื่องจักรที่ดีกว่านี้ นักวิชาการ Wang Dezhao ซึ่งขณะนั้นเป็นผู้อำนวยการสถาบันเสียงของ Chinese Academy of Sciences ได้ให้คำแนะนำแก่ Wu Wenjun เขาบอก Wu Wenjun ว่า Li Chang เลขาธิการกลุ่มปาร์ตี้และรองประธาน Chinese Academy of Sciences จะปรากฏตัวเมื่อใดและที่ไหน แต่ Wu Wenjun จับเขาได้จริงๆ Li Chang เป็นคนใจกว้าง เมื่อเขาดำรงตำแหน่งประธานของ Harbin Institute of Technology (ต่อไปนี้จะเรียกว่า "HIT") ในปี 1950 เขาเปลี่ยน HIT ให้เป็นมหาวิทยาลัยระดับเฟิร์สคลาสแห่งชาติ ในบรรดาหกมหาวิทยาลัยหลักระดับชาติที่ระบุในปี 1954 สถาบันเทคโนโลยีฮาร์บินเป็นมหาวิทยาลัยเดียวที่ไม่ได้ตั้งอยู่ในปักกิ่ง Li Chang ยังให้การสนับสนุนงานของ Wu Wenjun เป็นอย่างดี เงินแลกเปลี่ยนต่างประเทศของ Wu Wenjun จำนวน 25,000 ดอลลาร์สหรัฐเพื่อซื้อคอมพิวเตอร์ในสหรัฐอเมริกาได้รับการอนุมัติเป็นพิเศษจาก Li Chang ด้วยคอมพิวเตอร์เครื่องนี้ ทฤษฎีบทมากมายได้รับการพิสูจน์อย่างรวดเร็ว

ทศวรรษที่ 1970 ยังเป็นยุคทองของการพิสูจน์ทฤษฎีบทเครื่องจักรอีกด้วย ในปี พ.ศ. 2519 นักคณิตศาสตร์ชาวอเมริกันสองคนพิสูจน์ทฤษฎีบทสี่สีโดยใช้คอมพิวเตอร์อิเล็กทรอนิกส์ความเร็วสูงที่มีเวลาในการคำนวณ 1200 ชั่วโมง และแก้ปัญหายากที่นักคณิตศาสตร์แก้ไม่ได้มานานกว่า 100 ปี เหตุผลที่สามารถพิสูจน์ทฤษฎีบทสี่สีได้ก็คือเซตที่ลดไม่ได้และเซตที่หลีกเลี่ยงไม่ได้นั้นมีจำกัด ปัญหา "การลงสีแผนที่" ของทฤษฎีบทสี่สีดูเหมือนจะมีแผนที่มากมายนับไม่ถ้วน รูปร่างพื้นฐาน 2,000 ชนิดจากนั้นใช้พลังการคำนวณของคอมพิวเตอร์เพื่อบังคับเดรัจฉานและพิสูจน์พวกมันทีละตัว การพูดในเชิงเปรียบเทียบ วิธีนี้เหมือนกับการแก้ลูกบาศก์ของรูบิค—การแยกลูกบาศก์ออกจากกันและประกอบกลับเข้าไปใหม่—ไม่สวยงามแต่ได้ผล ตอนนี้เรากล่าวว่า GPT-3 "สร้างปาฏิหาริย์ด้วยความพยายามอย่างยิ่งยวด" แต่ในความเป็นจริงแล้วการพิสูจน์ทฤษฎีบทสี่สีคือบรรพบุรุษของ "ปาฏิหาริย์ด้วยความพยายามอย่างยิ่งยวด"

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

ดังนั้น หลังจากพิสูจน์ทฤษฎีบทสี่สีด้วยคอมพิวเตอร์ นักตรรกวิทยากลุ่มหนึ่งรวมถึง Wang Hao ได้เสนอความคิดเห็นที่แตกต่างกัน: ทฤษฎีบทสี่สีได้รับการพิสูจน์แล้วหรือไม่? วิธีการพิสูจน์แบบนี้ถือเป็นการพิสูจน์แบบดั้งเดิม และคอมพิวเตอร์มีบทบาทในการคำนวณเสริมเท่านั้น จนกระทั่งในปี 2548 Georges Gonthier ได้เสร็จสิ้นการพิสูจน์ทฤษฎีบทสี่สีด้วยคอมพิวเตอร์อย่างสมบูรณ์ และทุกขั้นตอนของรากเหง้าเชิงตรรกะนั้นเสร็จสมบูรณ์ด้วยคอมพิวเตอร์ ในปัจจุบัน ผู้คนได้พิสูจน์ทฤษฎีบททางคณิตศาสตร์หลายร้อยรายการด้วยคอมพิวเตอร์ แต่ส่วนใหญ่รู้จักทฤษฎีบทเหล่านี้ และ "ความฉลาดของเครื่องจักร" ยังไม่ได้มีส่วนช่วยในวิชาคณิตศาสตร์อย่างแท้จริง

การพิสูจน์ทฤษฎีบทของเครื่องอาศัยอัลกอริธึม ในระยะแรก นักวิจัยมักจะพยายามค้นหาอัลกอริธึมขั้นสูงเพื่อแก้ปัญหาทั้งหมด แต่ Wu Wenjun ได้นำแนวคิดทางคณิตศาสตร์ของจีนโบราณมาใช้ในสาขาการพิสูจน์ด้วยเครื่องจักรของทฤษฎีบทเรขาคณิต ทำให้ได้ "หนึ่งประเภท หนึ่งการพิสูจน์" จุดนี้เห็นด้วยโดย Wang Hao เขาเชื่อว่างานในช่วงแรกของเขามีบางอย่างที่เหมือนกันกับวิธีการที่ Wu Wenjun ใช้ นั่นคือ ก่อนอื่นให้ค้นหาฟิลด์ย่อยที่ควบคุมได้ค่อนข้างดี ฟิลด์ย่อย เมื่อ Wu Wenjun ไปเยือนสหรัฐอเมริกาในปี 1979 เขายังไปที่ Rockefeller University เพื่อเยี่ยมชม Wang Hao งานของเขามีคุณค่าในด้านทฤษฎีบทเครื่องจักรซึ่งมีความสัมพันธ์บางอย่างกับคำแนะนำที่หนักแน่นของ Wang Hao

"วิธีการของ Wu" แพร่กระจายอย่างมาก ทำให้เกิดความก้าวหน้าครั้งแรกในทฤษฎีบทเครื่องจักรที่พิสูจน์ได้ในทศวรรษที่ 1980 ขอบคุณ Zhou Xianqing นักศึกษาต่างประเทศในสหรัฐอเมริกาที่ได้ฟังหลักสูตรการพิสูจน์ทฤษฎีบทเครื่องจักรของ Wu Wenjun เดิมที Zhou Xianqing ต้องการรับปริญญาบัณฑิตของ Wu Wenjun ในสาขาการพิสูจน์เครื่องจักร แต่เขาคิดว่าเรขาคณิตเชิงอนุพันธ์เป็นจุดอ่อนของเขา ดังนั้นเขาจึงกลัวว่าเขาจะสอบไม่ผ่าน ดังนั้นในที่สุดเขาจึงได้เข้าเรียนในมหาวิทยาลัย ของวิทยาศาสตร์และเทคโนโลยีแห่งประเทศจีน (ต่อไปนี้จะเรียกว่า "มหาวิทยาลัยวิทยาศาสตร์และเทคโนโลยีแห่งประเทศจีน") และต่อมาได้ไปที่สถาบันเทคโนโลยีคอมพิวเตอร์ของสถาบันวิทยาศาสตร์จีนในชื่อ Dai Pei ในเรื่องนี้ ฉันได้ตรวจสอบรูปทรงเรขาคณิตของ Wu Wenjun หลักสูตรพิสูจน์

ในปี 1981 Zhou Xianqing เดินทางไปศึกษาต่อที่มหาวิทยาลัย Texas at Austin ในเวลานั้น University of Texas at Austin เป็นที่รู้จักในฐานะราชาแห่งการพิสูจน์ทฤษฎีบท Zhou Xianqing พูดถึงงานของ Wu Wenjun กับ Robert Boyer Boyer คิดว่ามันใหม่มาก ดังนั้นเขาจึงถามต่อไป แต่ Zhou Xianqing รู้แค่ว่ามันกำลังเปลี่ยนรูปทรงเรขาคณิตเป็นพีชคณิตและไม่สามารถอธิบายรายละเอียดเฉพาะเจาะจงได้

หลังจากนั้น Woody Bledsoe ขอให้ Zhou Xianqing และนักเรียนคนอื่น Wang Tiecheng รวบรวมข้อมูล วิทยานิพนธ์ระดับปริญญาเอกของ Zhou Xianqing เป็นการทำให้วิธีการของ Wu เป็นจริง อู๋ เหวินจุนรีบส่งบทความสองเรื่อง ซึ่งทั้งสองบทความเขาเซ็นให้ Bledsoe ในอีกสองปีข้างหน้า บทความทั้งสองนี้ถูกคัดลอกโดยมหาวิทยาลัยเทกซัสที่ออสตินเกือบร้อยครั้งและถูกส่งไปทั่วโลก และวิธีการของ Wu ก็เป็นที่รู้จักอย่างกว้างขวาง

ในปี 1983 การประชุมวิชาการระดับชาติเกี่ยวกับการพิสูจน์ทฤษฎีบทโดยเครื่องจักรจัดขึ้นที่โคโลราโด สหรัฐอเมริกา Zhou Xianqing ได้จัดทำรายงานเรื่อง "Proving Geometry Theorems using Wu's Method" ในการประชุม โปรแกรมทั่วไปที่พัฒนาโดย Zhou Xianqing สามารถพิสูจน์ทฤษฎีบททางเรขาคณิตได้มากกว่า 130 โดยอัตโนมัติ รวมถึงการพิสูจน์ทฤษฎีบทที่ยากขึ้น เช่น ทฤษฎีบทของ Moller ทฤษฎีบทของ Simson ทฤษฎีบทวงกลมเก้าจุดของ Feuerbach และทฤษฎีบทของ Desargues หลังจากนั้น การรวบรวมเอกสารของการประชุมนี้ได้รับการตีพิมพ์อย่างเป็นทางการในปี 1984 ในชื่อชุด "Contemporary Mathematics" เล่มที่ 29 ในสหรัฐอเมริกา และเอกสารที่เกี่ยวข้องสองฉบับที่ส่งโดย Wu Wenjun ก็รวมอยู่ในนั้นด้วย

ในเดือนมิถุนายน พ.ศ. 2529 จอห์น ฮอปครอฟต์ ผู้ได้รับรางวัลทัวริง (John Hopcroft) และคนอื่นๆ ได้จัดสัมมนาเกี่ยวกับการให้เหตุผลทางเรขาคณิตโดยอัตโนมัติ และส่วนหนึ่งของรายงานการสัมมนารวมอยู่ใน "สิ่งประดิษฐ์ในฉบับพิเศษของ "ข่าวกรอง" บทความแนะนำของ ฉบับพิเศษแนะนำวิธีการใหม่ของเรขาคณิตพีชคณิตที่เสนอโดย Wu Wenjun วิสัยทัศน์ การสร้างแบบจำลองแบบทึบ) ก็มีค่าการใช้งานที่สำคัญเช่นกัน (รูปที่ 1-2) ตั้งแต่นั้นมา Hopcroft ก็ได้ทำงานอย่างใกล้ชิดกับมหาวิทยาลัยต่างๆ ในประเทศจีน เขามีสถาบันวิจัยที่นำโดยเขาใน Shanghai Jiao Tong University, Peking University และ Chinese University of Hong Kong (Shenzhen) Wu Wenjun และ Wu Fafang น่าจะเป็นจุดเริ่มต้นของ คอมเพล็กซ์จีนของเขา

รูปที่ 1-2 ภาพรวมของวิธีการของ Wu ในบทเริ่มต้นของ "Artificial Intelligence" ฉบับพิเศษในปี 1988