Axiom Math는 유한 단순군 분류 정리를 Lean으로 형식화한 약 4310만 줄의 코드를 공개했다고 밝혔다. 수학자와 엔지니어가 AI 에이전트를 지휘해 24일간 작업했으며, 기존 문헌과 달라진 중요한 부분 34건을 해결했다는 설명이다. 공개 저장소는 미완성 증명 표시 없이 표준 공리만 사용한다고 명시한다. 이는 회사의 발표와 코드 공개를 확인한 것으로, 이 거대한 프로젝트를 독립적으로 다시 빌드하거나 모든 정의가 원래 수학과 정확히 대응하는지 검토한 결과는 아니다.