การพิสูจน์ทฤษฎีทางคณิตศาสตร์ให้มีความถูกต้องระดับร้อยเปอร์เซ็นต์มักต้องใช้ความพยายามอย่างมหาศาล แต่งานวิจัยนี้แสดงให้เห็นว่า AI สามารถเข้ามาช่วยในขั้นตอนนี้ได้ผ่านระบบ AutoIP ซึ่งเป็นคลังความรู้ที่สร้างขึ้นบนภาษาโปรแกรม Lean (Proof Assistant) โดย AI ได้ทำการ 'Autoformalize' ทฤษฎีบทเกี่ยวกับการปรับปรุงสมดุลเชิงเส้น (Linear Regularization) และการวิเคราะห์เชิงฟังก์ชัน (Functional Analysis)
ความโดดเด่นคือการเปลี่ยนบทบาทของมนุษย์ จากเดิมที่ต้องเป็นผู้เขียนพิสูจน์เอง มาเป็นเพียงผู้ตรวจทาน 'คำกล่าวอ้าง' (Formal Statements) ให้ตรงกับภาษาธรรมชาติเท่านั้น เนื่องจากเครื่องจักรจะเป็นผู้ยืนยันความถูกต้องของขั้นตอนการพิสูจน์ให้ นอกจากนี้ ระบบยังสามารถระบุข้อบกพร่องในตำราคณิตศาสตร์มาตรฐานที่มีการตั้งสมมติฐานที่เคร่งครัดเกินความเป็นจริงได้อีกด้วย
