AHM เรียกร้องให้นักคณิตศาสตร์คว่ำบาตร OpenAI หลังปล่อยพรูฟ Lean 722 ฉบับ โดยมี Terence Tao ร่วมเผยแพร่แถลงการณ์
การปล่อยข้อพิสูจน์คณิตศาสตร์แบบอัตโนมัติปริมาณมหาศาลโดยไม่มีการคัดกรองจากมนุษย์ สร้างภาระการตรวจสอบอย่างหนักหน่วงและอาจนำไปสู่ข้อผิดพลาดเชิงโครงสร้างสำหรับงานวิจัยและโมเดลธุรกิจที่ต้องพึ่งพาความแม่นยำสูง