งานวิจัยนี้เสนอแนวทางการพิสูจน์ทฤษฎีบททางคณิตศาสตร์ระดับสูงในรูปแบบทางการ (Formalization) โดยใช้ AI เป็นผู้ช่วยในระบบ Lean 4 proof assistant ซึ่งทีมวิจัยได้พิสูจน์ความถูกต้องของ Vlasov equation ผ่านกระบวนการที่เรียกว่า "Formalization Game" มนุษย์จะรับหน้าที่เป็นผู้กำกับ (Director) ในการกำหนดนิยาม แยกองค์ประกอบของปัญหา และจัดการช่องว่างในคลังฟังก์ชัน (Library) ในขณะที่ AI จะรับหน้าที่เป็นเอเจนต์ผู้ลงมือเขียนรหัสข้อพิสูจน์ให้สอดคล้องตามกฎเกณฑ์
ผลลัพธ์ที่ได้คือการรับรองความถูกต้องของข้อพิสูจน์คณิตศาสตร์ที่ซับซ้อนได้อย่างสมบูรณ์ โดยไม่เหลือส่วนที่ยังพิสูจน์ไม่เสร็จ (no sorry) และใช้เวลาในการพัฒนาเพียงประมาณหนึ่งเดือน ซึ่งเร็วกว่าการทำด้วยมนุษย์เพียงอย่างเดียวอย่างมาก นอกจากนี้ งานวิจัยยังได้สร้างคลังความรู้ทางคณิตศาสตร์ทั่วไป (General Mathematics) ที่สามารถนำไปใช้ซ้ำในโปรเจกต์อื่นๆ ต่อไปได้
