นักคณิตศาสตร์โลกแนะเทรนด์ใหม่ ใช้ "โปรแกรมคอมพิวเตอร์ช่วยพิสูจน์" ตรวจสมการซับซ้อนยากเย็นง่ายในพริบตา ดึงไอทีเสริมงานวิจัย ลดภาระงานนักคณิตศาสตร์ระดับสูง มิติใหม่วงการคำนวณ
ในโอกาสมาเยือนประเทศไทย ศ.ดร.วลาดิเมีย โวอิวอดสกี (Professor Vladimir Voevodsky) ผู้ได้รับรางวัลเหรียญฟิล์ด (Fields Medal) ซึ่งเป็นรางวัลสูงสุดด้านคณิตศาสตร์เทียบเท่ารางวัลโนเบลประจำปี พ.ศ. 2545 และผู้วางรากฐานคนสำคัญในการพัฒนา Homotopy Type Theory (HoTT) ได้ร่วมบรรยายพิเศษเรื่อง Computer Proof Assistants – the future of mathematics ตามคำเชื้อเชิญของคณะวิทยาศาสตร์ มหาวิทยาลัยมหิดล เพื่อเปิดมิติใหม่ด้านการวิจัยแก่คณาจารย์ บุคลากร นักศึกษาและบุคลทั่วไป
ศ.ดร.วลาดิเมีย กล่าวว่า คอมพิวเตอร์ช่วยพิสูจน์ เป็นแนวทางใหม่สำหรับการทำวิจัยทางด้านคณิตศาสตร์ในอนาคต เพราะคณิตศาสตร์เป็นทั้งศาสตร์และศิลป์ของการให้เหตุผลเชิงนามธรรม ถ้าการพิสูจน์สั้นและไม่ซับซ้อนการตรวจสอบความถูกต้องย่อมทำได้ไม่ยากนัก แต่ในการพิสูจน์ข้อสรุปทางคณิตศาสตร์ที่ต้องใช้ความรู้หลากหลายซับซ้อน จะทำให้เกิดปัญหาในการตรวจสอบความถูกต้อง แม้จะใช้ผู้ตรวจที่เป็นผู้เชี่ยวชาญ
การใช้คอมพิวเตอร์เข้ามาช่วยในการตรวจสอบพิสูจน์จึงเป็นอีกทางเลือกหนึ่งในการแก้ปัญหา ซึ่งการตรวจสอบความถูกต้องของการพิสูจน์ทฤษฎีบทที่ซับซ้อนผ่าน "ทฤษฎีโฮโมไทป์" (Homotopy Type Theory : HoTT) ที่เป็นการทำงานด้วยโปรแกรมคอมพิวเตอร์ จะทำให้การตรวจสอบการพิสูจน์ หรือแม้แต่ช่วยในการพิสูจน์มีประสิทธิภาพมากขึ้น
"ผมจึงหวังว่าในอนาคตต่อจากนี้ จะเห็นการพัฒนาทั้งทางด้านการเขียนโปรแกรมคอมพิวเตอร์ และงานวิจัยทางคณิตศาสตร์ไปพร้อมๆกัน" ศ.ดร.วลาดิเมีย เผย
ด้าน ดร.ชัชวาล ปานรักษา อาจารย์ประจำวิทยาลัยนานาชาติมหาวิทยาลัยมหิดล กล่าวแก่ทีมข่าวผู้จัดการวิทยาศาสตร์ว่า ทฤษฎีโฮโมไทป์ เป็นทฤษฎีใหม่ที่เพิ่งมีการนำมาใช้สอบพิสูจน์ทฤษฎีบทยากๆ เช่น ทฤษฎีบทของเฟทและทอมป์สัน (Feit and Thompson theorem) ซึ่งซับซ้อน ต้องพิสูจน์ด้วยความยาวกระดาษกว่าหลายร้อยหน้า ตั้งแต่ประมาณ 3 ปีก่อน
ทว่าทฤษฎีนี้นักคณิตศาสตร์สนใจมานานเป็น 10 ปีแล้ว แต่เพิ่งได้รับความสนใจดย่างมากเมื่อปี 2556 เพราะ ศ.วลาดิเมีย ได้นำไอเดียทางด้านตรรกศาสตร์, วิทยาการคอมพิวเตอร์, ปรัชญา รวมไปถึงเลขาคณิตวิเคราะห์มาผนวกไว้ด้วยกัน จนทำให้การพิสูจน์ทฤษฎีบททางคณิตศาสตร์ด้วยคอมพิวเตอร์ได้รับการยอมรับมากยิ่งขึ้น
"การมาบรรยายครั้งนี้จะเป็นประโยชน์มากกับอาจารย์และนักศึกษาที่สนใจส่วนงานด้านคณิตศาสตร์วิเคราะห์ เพราะ ศ.วลาดิเมียเป็นนักคณิตศาสตร์ระดับโลกที่ใครๆ ก็อยากได้ฟังประสบการณ์ของเขา ซึ่งครั้งนี้เป็นโอกาสเหมาะเนื่องจากเขาเดินทางมาร่วมพิธีเปิดค่ายวิทยาศาสตร์ฤดูร้อนอาเซียน (Asian Science Camp) พอดี ทางมหิดลจึงเชิญมาเพื่อให้บุคลากรและคนทั่วไปได้มีโอกาสใกล้ชิดกับนักวิจัยระดับโลก ซึ่งเราจัดอยู่เป็นประจำ" ดร.ชัชวาล เผย
ด้าน นายศรัญย์ อินทะผิว บัณฑิตหมาดๆ จากภาควิชาคณิตศาสตร์ คณะวิทยาศาสตร์ มหาวิทยาลัยมหิดลพร้อมเพื่อนได้เผยกับทีมข่าวผู้จัดการวิทยาศาสตร์ด้วยว่า แม้จะฟังไม่ได้รู้เรื่องทั้งหมดแต่ก็รู้สึกดีที่ได้มีโอกาสใกล้ชิดกับนักคณิตศาสตร์ระดับโลก ได้อัพเดตว่าขณะนี้วงการคณิตศาสตร์โลกก้าวหน้าไปถึงไหน และได้รู้จักกับวิธีการจัดการทฤษฎีบทใหม่ๆ ด้วยคอมพิวเตอร์ เพราะเขาซึ่งอยู่ในแวดวงทราบดีว่า การพิสูจน์ทฤษฎีบทใหม่แต่ละครั้งไม่ใช่เรื่องง่าย ต้องใช้ผู้เชี่ยวชาญระดับสูง ซึ่งเทคโนโลยีนี้จะทำให้วงการคณิตศาสตร์ก้าวหน้าไปอีกขั้น
เช่นเดียวกับนายภควุฒิ จิรดิลก นักเรียนทุนเล่าเรียนหลวงสายวิทยาศาสตร์ประจำปี 2555 ซึ่งขณะนี้เป็นนักศึกษาระดับปริญญาตรี มหาวิทยาลัยฮาร์วาร์ด สหรัฐฯ ที่เผยกับทีมข่าวฯ ว่าตั้งใจเดินทางมาฟังเพื่อหาแรงบันดาลใจ เพราะ ศ.วลาดิเมีย เป็นนักคณิตศาสตร์ที่มีชื่อเสียงอันดับต้นๆ ของโลก ซึ่งเป็นหนึ่งในไอดอลของเขา
นายภควุฒิ กล่าวว่า สิ่งที่ ศ.วลาดิเมีย อธิบายเกี่ยวกับการใช้คอมพิวเตอร์เข้ามาช่วยจัดการพิสูจน์ทฤษฎีบทเป็นเรื่องที่น่าสนใจ เพราะจากประสบการณ์ที่สัมผัสกับการเรียนในต่างประเทศมา ทำให้ทราบว่าการตรวจสอบพิสูจน์ทฤษฎีบทหนึ่งๆ นั้นยากพอๆ กับการคิดทฤษฎี ซึ่งหากคอมพิวเตอร์เข้ามาช่วยจัดการได้ก็จะช่วยให้การทำงานลดความซับซ้อนลงไปได้อีกมาก เพราะคอมพิวเตอร์สามารถทำงานที่ซับซ้อนได้มากและยาวนานกว่ามนุษย์ ซึ่งมนุษย์ที่เก่งคณิตศาสตร์มากๆ ในโลกก็ไม่ได้มีมากเช่นกัน คอมพิวเตอร์จึงเป็นทางออกที่ดี
"ตัวผมไม่ได้เรียนด้านที่ ศ.เขาทำงานเท่าไรเลยแค่พอเข้าใจ ไม่ได้สันทัดมากนัก แต่ที่มาในวันนี้คือผมจะมาเอาพลัง เพราะผมอยากเป็น อยากเก่งแบบเขา การได้มาใกล้ชิดกับนักคณิตศาสตร์ไอดอลตัวเป็นๆ มันทำให้ผมมีแรงฮึดว่าเขาทำได้ ผมก็ต้องทำได้ เป็นเครื่องยืนยันทางจิตใจสำหรับเด็กนักเรียนตัวเล็กๆ ที่มีความฝันอย่างผม เหมือนการไปดูคอนเสิร์ตนักร้องที่ตัวเองชอบ มันย่อมได้อะไรมากกว่าการเปิดยูทิวป์ดูอยู่ที่บ้านอยู่แล้ว" ภควุฒิ กล่าวแก่ทีมข่าวผู้จัดการวิทยาศาสตร์ว่า
ท้ายสุด ภควุฒิ ยังกล่าวด้วยว่า ที่ต้องมาหากำลังใจให้ตัวเองมากๆ นั้น เป็นเพราะสังคมไทยส่วนใหญ่ยังไม่เข้าใจและไม่เปิดใจกับการเรียนคณิตศาสตร์ ยังไม่เข้าใจว่าจะเรียนคณิตศาสตร์สูงๆ ไปทำไม มีประโยชน์อะไร แถมยังมีทุนวิจัยอยู่ไม่มากเหมือนกับประเทศพัฒนาแล้วเช่น ญี่ปุ่น การจะยืนหยัดเพื่อเป็นนักคณิตศาสตร์ระดับโลกตามความฝันของเขาจึงต้องอาศัยแรงบันดาลใจของตัวเองและความเชื่อมั่นของคนในครอบครัวสูงมาก
ทั้งนี้การบรรยายพิเศษ เรื่อง Computer Proof Assistants – the future of mathematics จัดขึ้นเมื่อวันที่ 4 ส.ค. 2558 ณ ห้องประชุมสตางค์ มงคลสุข คณะวิทยาศาสตร์ มหาวิทยาลัยมหิดล พญาไท
*******************************
