นักคณิตศาสตร์รางวัลโนเบลด้านคณิตศาสตร์ บรรยายพิเศษ เรื่อง Computer Proof Assistants – the Future of Mathematics

เมื่อวันอังคารที่ 4 สิงหาคม 2558 เวลา 15.30 น. ณ ห้องประชุมสตางค์ มงคลสุข คณะวิทยาศาสตร์ มหาวิทยาลัยมหิดล พญาไท ผู้ช่วยศาสตราจารย์ ดร. สมคิด อมรสมานกุล รองคณบดี ฝ่ายการศึกษา คณะวิทยาศาสตร์ มหาวิทยาลัยมหิดล เป็นประธานเปิด การบรรยายพิเศษ เรื่อง Computer Proof Assistants – the Future of Mathematics ซึ่งเกี่ยวกับการใช้คอมพิวเตอร์ในการช่วยพิสูจน์ ซึ่งเป็นแนวทางใหม่สำหรับการทำวิจัยทางด้านคณิตศาสตร์ในอนาคต โดย ศาสตราจารย์ Vladimir Voevodsky ผู้ได้รับรางวัล Fields Medal (รางวัลสูงสุดทางด้านคณิตศาสตร์ซึ่งมักจะถูกเรียกว่าเป็นรางวัลโนเบลสำหรับนักคณิตศาสตร์) ในปี 2002 และเป็นผู้วางรากฐานคนสำคัญในการพัฒนา Homotopy Type Theory (HoTT)

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

เนื่องจากหลายทฤษฎีบทต้องใช้เวลานานในการตรวจสอบความถูกต้อง อย่างเช่น ทฤษฎีบทสุดท้ายของแฟร์มา (Fermat Last Theorem) ที่มีการค้นพบความผิดพลาดโดยผู้เชี่ยวชาญภายหลังจากที่มีข่าวการพิสูจน์ไปเรียบร้อยแล้ว ต้องมีการแก้ไขโดยใช้เวลาพอสมควร การใช้คอมพิวเตอร์มาช่วยในการตรวจสอบการพิสูจน์นั้นเป็นอีกทางเลือกหนึ่งในการแก้ปัญหาการตรวจสอบความถูกต้องของการพิสูจน์ทฤษฎี ดังนั้นการใช้คอมพิวเตอร์เข้ามาช่วยในการตรวจสอบจึงเป็นทางเลือกหนึ่งในการแก้ปัญหา ซึ่งวิธีการที่จะทำให้การตรวจสอบการพิสูจน์หรือแม้แต่ช่วยในการพิสูจน์ให้มีประสิทธิภาพมากขึ้นผ่าน Homotopy Type Theory (HoTT) นับเป็นการค้นพบที่ทำให้เกิดความหวังที่จะมีการพัฒนาทั้งทางด้านการเขียนโปรแกรมคอมพิวเตอร์และงานวิจัยทางคณิตศาสตร์ไปพร้อมๆกัน

โดยมีผู้บริหาร คณาจารย์ นักศึกษา และผู้สนใจ เข้าร่วมฟังกว่า 100 คน