थिओडोर चाओ ने एआई उपकरणों का उपयोग करके गणितीय अनुमान का औपचारिक प्रमाण सफलतापूर्वक किया

थिओडोर चाओ ने एआई उपकरणों का सफलतापूर्वक उपयोग करके बहुपद फ्रेमैन-रुज़्सा अनुमान का औपचारिक प्रमाण करने में सफलता प्राप्त की है, जिसने गणित समुदाय का व्यापक ध्यान आकर्षित किया है। उन्होंने ब्लीप्रिंट का उपयोग करके Lean4 में औपचारिक प्रमाण की प्रक्रिया को विस्तृत रूप से दर्ज किया, और एआई उपकरणों का सही उपयोग करने के महत्व पर जोर दिया। ब्लीप्रिंट उपकरण का उपयोग करते हुए, चाओ टीम ने प्रमाण प्रक्रिया को तोड़कर, कई योगदानकर्ताओं के समांतर कार्य के माध्यम से PFR अनुमान को सफलतापूर्वक औपचारिक रूप दिया। चाओ का मानना है कि औपचारिक प्रमाण का मुख्यधारा में आना या ऐसे प्रमाण बनाना जो मानव-पाठ्य और मशीन-समाधेय दोनों हों, गणित के विकास को बदलेगा।