Axiom, 유한 단순군 분류를 24일 만에 Lean으로 형식화
수학 AI 기업 Axiom은 AxiomProver 에이전트 군집이 유한 단순군 분류 정리를 24일 만에 Lean으로 형식화해, 최초의 완전한 컴퓨터 검증 증명을 내놓았다고 밝혔다. 과정에서 34건의 수학적 편차도 발견됐다.
형식 검증 뉴스와 분석
형식 검증 관련 제품 동향과 산업 분석 6건을 모았습니다.
Claude, 오픈소스 123개에 어셈블리 수준 증명 작성
Anthropic 프런티어 레드팀이 Claude로 오픈소스 라이브러리 123개, 239개 진입점이 64MB 미만 입력에서 중단되지 않음을 컴파일된 RISC-V 바이너리 위에서 형식 증명했다.
페르마의 마지막 정리, Lean 4로 완전 기계검증
Anthropic이 페르마의 마지막 정리를 Lean 4로 완전히 기계검증한 증명을 Apache 2.0으로 공개했다. Mathlib 위에 구축됐고 3중 검증기로 확인했다.
버클리 Vero 벤치마크, 43개 중 27개만 완전 해결
버클리 RDI 연구소의 새 벤치마크 Vero는 AI 에이전트에게 Lean 4 저장소 전체 규모의 구현과 증명을 동시에 요구한다. 최고 성능 모델조차 43개 프로젝트 중 27개만 완전히 풀어냈다.
OpenBMB, 8B 형식화 모델로 32B 압도해 공개
OpenBMB가 수학 자동 형식화 파이프라인 MathForm을 통째로 공개했다. 8B 모델과 검증된 Lean 4 데이터 약 36만 7000건, 평가 코드까지 무료로 풀었고 여러 32B 전용 모델을 앞질렀다.
OpenAI, Astra로 증명 10건 공개
OpenAI는 Astra의 첫 공개 신호로 수학과 이론 컴퓨터과학의 10개 결과, 249쪽 논문, Lean 증명서와 추론 기록을 공개했다.