최근 몇 달 동안 다양한 오래되고 새로운 결과에 대한 AI 생성 증명이 확산되었으며, 그중 일부는 증명 보조 언어인 Lean으로 형식화되었습니다. 그러나 주어진 Lean 저장소가 실제로 주장된 명제를 증명하는지 확인하는 것은 다소 간단하지 않은데, 특히 사용 전문가가 아닌 청중에게는 더욱 그렇습니다.