OpenAI의 수학 저장소가 핵심 계산의 부호 오류로 논문 한 편과 그 결과에 의존한 두 편을 철회했다고 기록했다. 해당 논문의 수정 공지는 계산값이 예상과 달라 정리의 가정을 충족하지 못한다고 설명한다. 함께 공개된 진행 보고에는 새 Lean 형식화 6건과 전체 719개 중 300개, 약 42%의 형식화 현황도 담겼다. 형식화 진척과 철회는 별개의 지표이며, 철회는 기존 증명이 성립하지 않는다는 뜻이지 명제의 거짓을 확정한 것은 아니다.