PaperFormalizer เป็นระบบ Agentic Pipeline ที่ออกแบบมาเพื่อช่วยให้นักวิจัยสามารถค้นหาช่องโหว่เล็กๆ ในบทพิสูจน์หรือสมมติฐานของงานวิจัย โดยอาศัยภาษา Lean ซึ่งเป็นภาษาสำหรับการตรวจสอบบทพิสูจน์ทางคณิตศาสตร์ที่เข้มงวด
ระบบจะเริ่มจากการอ่านซอร์สโค้ด LaTeX และสร้างกราฟความสัมพันธ์ของข้อความ จากนั้นจะใช้ AI ตรวจสอบความกำกวมและความถูกต้องเบื้องต้น ก่อนจะทำการแปลงเป็นภาษา Lean โดยมีการทำงานร่วมกับผู้เขียน (Author-in-the-loop) หากพบว่าข้อความใดสามารถตีความได้หลายแบบ AI จะเสนอแนวทางการแก้ไขให้ผู้เขียนเลือกหรือปรับปรุงได้ทันที
นอกจากจะช่วยให้งานวิจัยมีความน่าเชื่อถือมากขึ้นแล้ว ระบบนี้ยังช่วยสร้างคลังโค้ดภาษา Lean ที่นักวิจัยคนอื่นสามารถนำไปใช้งานต่อได้ โดยปัจจุบันเครื่องมือนี้รองรับการใช้งานผ่าน Claude Code และ Codex
