Anthropic은 2026년 9월 4일 내부 모델 중 하나가 prove2.me 플랫폼을 사용해 Lean에서 페르마의 마지막 정리 전체 증명을 공식화했다고 공식 발표했다. Xena Project 게시물에 따르면 이 결과는 주요 수학 성과를 기계가 검증할 수 있는 증명으로 바꾸는 20년 된 벤치마크인 Freek Wiedijk의 100개 공식화 과제 목록에서 마지막 항목을 완료한 것이다. 해당 소식은 Anthropic 발표 약 1시간 전, Islington의 한 커피숍 인스타그램을 통해 먼저 알려졌다고 게시물은 전했다.

공식화된 증명은 Xena Project 저자가 Khare와 Taylor의 아이디어를 따라 공식화하던 현대적 증명이 아니라, 1995년 Darmon-Diamond-Taylor가 정리한 Wiles-Taylor-Wiles 논증을 따른다. Anthropic 저장소는 Fontaine 이론과 Eisenstein ideal에 관한 Mazur의 작업 중 충분한 부분을 전개해, 어떤 차수의 점을 가진 Frey 곡선을 배제한다. 저자는 이 버전이 37 이상인 소수를 다루며, 홀수 정규 소수에 대해서는 Best-Birkbeck-Brasca-Rodriguez-van-der-Velde-Yang이 이미 페르마의 마지막 정리를 공식화했다고 설명했다. 가장 작은 비정규 소수는 37이다.

Xena Project 저자는 Anthropic 코드베이스를 컴파일하고 comparator를 실행했으며, 검증이 통과됐다고 밝혔다. 저장소는 1,340만 줄이 넘는 거대한 증명으로 묘사됐고, 96코어 장비에서 Lean의 수학 라이브러리보다 컴파일 시간이 거의 20배 더 걸렸다. Anthropic이 제공한 500G ram 장비에서도 그 규모의 저장소에서는 파일 사이를 이동할 때 Lean이 느렸기 때문에, Anthropic은 실제 탐색이 더 쉬운 HTML 문서도 함께 제공했다.

Xena Project 저자는 이 결과가 자신의 EPSRC 지원 페르마의 마지막 정리 작업을 끝내는 것은 아니라고 말했다. 그는 5년간 £1M을 받았고, Lean의 수학 라이브러리에 현대 정수론 객체를 추가하며 사람들이 현대적 증명을 탐색할 수 있는 동적 문서를 만들겠다고 약속했었다. 저자는 Anthropic 저장소가 전체 정리를 증명하고 FLT를 1980년대 수준으로 환원하겠다는 자신의 약속을 넘어섰지만, 현대적 증명을 공식화하거나 사람을 위한 문서를 만든 것은 아니라고 설명했다.

저자는 이번 공식화가 수학적으로는 사실상 아무것도 더하지 않는다고 평가했다. 그는 이미 페르마의 마지막 정리 증명이 맞다고 99.9% 확신했으며, 대부분의 정수론자는 100% 확신한다고 말했다. 다만 저자가 보는 중요성은 자동 공식화에 있다. 수천 쪽의 문헌을 AI swarm이 11일 동안 처음부터 끝까지 공식화할 수 있다면, 기계가 언젠가 현대 연구가 작성되는 시점에 이를 검증하고 수학 논문 속 불완전한 논증을 표시할 수 있다는 것이다.

Anthropic은 2026년 9월 4일 내부 모델 중 하나가 prove2.me 플랫폼을 사용해 Lean에서 페르마의 마지막 정리 전체 증명을 공식화했다고 공식 발표했다. Xena Project 게시물에 따르면 이 결과는 주요 수학 성과를 기계가 검증할 수 있는 증명으로 바꾸는 20년 된 벤치마크인 Freek Wiedijk의 100개 공식화 과제 목록에서 마지막 항목을 완료한 것이다. 해당 소식은 Anthropic 발표 약 1시간 전, Islington의 한 커피숍 인스타그램을 통해 먼저 알려졌다고 게시물은 전했다.

공식화된 증명은 Xena Project 저자가 Khare와 Taylor의 아이디어를 따라 공식화하던 현대적 증명이 아니라, 1995년 Darmon-Diamond-Taylor가 정리한 Wiles-Taylor-Wiles 논증을 따른다. Anthropic 저장소는 Fontaine 이론과 Eisenstein ideal에 관한 Mazur의 작업 중 충분한 부분을 전개해, 어떤 차수의 점을 가진 Frey 곡선을 배제한다. 저자는 이 버전이 37 이상인 소수를 다루며, 홀수 정규 소수에 대해서는 Best-Birkbeck-Brasca-Rodriguez-van-der-Velde-Yang이 이미 페르마의 마지막 정리를 공식화했다고 설명했다. 가장 작은 비정규 소수는 37이다.

Xena Project 저자는 Anthropic 코드베이스를 컴파일하고 comparator를 실행했으며, 검증이 통과됐다고 밝혔다. 저장소는 1,340만 줄이 넘는 거대한 증명으로 묘사됐고, 96코어 장비에서 Lean의 수학 라이브러리보다 컴파일 시간이 거의 20배 더 걸렸다. Anthropic이 제공한 500G ram 장비에서도 그 규모의 저장소에서는 파일 사이를 이동할 때 Lean이 느렸기 때문에, Anthropic은 실제 탐색이 더 쉬운 HTML 문서도 함께 제공했다.

Xena Project 저자는 이 결과가 자신의 EPSRC 지원 페르마의 마지막 정리 작업을 끝내는 것은 아니라고 말했다. 그는 5년간 £1M을 받았고, Lean의 수학 라이브러리에 현대 정수론 객체를 추가하며 사람들이 현대적 증명을 탐색할 수 있는 동적 문서를 만들겠다고 약속했었다. 저자는 Anthropic 저장소가 전체 정리를 증명하고 FLT를 1980년대 수준으로 환원하겠다는 자신의 약속을 넘어섰지만, 현대적 증명을 공식화하거나 사람을 위한 문서를 만든 것은 아니라고 설명했다.

저자는 이번 공식화가 수학적으로는 사실상 아무것도 더하지 않는다고 평가했다. 그는 이미 페르마의 마지막 정리 증명이 맞다고 99.9% 확신했으며, 대부분의 정수론자는 100% 확신한다고 말했다. 다만 저자가 보는 중요성은 자동 공식화에 있다. 수천 쪽의 문헌을 AI swarm이 11일 동안 처음부터 끝까지 공식화할 수 있다면, 기계가 언젠가 현대 연구가 작성되는 시점에 이를 검증하고 수학 논문 속 불완전한 논증을 표시할 수 있다는 것이다.