Anthropic, Claude가 Lean에서 페르마의 마지막 정리 형식화를 도왔다고 공개

Anthropic이 Claude를 사용해 페르마의 마지막 정리를 Lean에서 형식화하는 연구를 공개했다. Lean은 수학적 논증을 한 줄씩 검사하는 증명 보조기다. 이번 발표는 모델이 새로운 증명을 독자적으로 발견했다는 이야기가 아니라, 인간이 압축적으로 작성한 어려운 증명을 기계가 검증할 수 있는 형식 코드로 옮기는 작업에서 AI가 어디까지 도울 수 있는지를 보여준다.

페르마의 마지막 정리는 수학사에서 가장 유명한 결과 중 하나다. Andrew Wiles가 1990년대에 증명했지만, 그 증명은 수론과 대수기하의 깊은 도구에 의존한다. 이런 규모의 결과를 형식화하는 일은 독자를 위한 설명문을 쓰는 것과 다르다. 정의, 의존 정리, 변환, 논리 단계가 모두 증명 보조기가 확인할 수 있을 만큼 명시되어야 한다. 전문가에게도 느리고 까다로운 공학 작업이다.

Anthropic은 글에서 Claude를 이 증명 공학 과정의 협업자로 설명한다. 모델은 Lean 코드를 제안하고, 수학적 문장을 형식 문법으로 옮기며, 오류를 수정하고, 중간 보조정리를 연결하는 방법을 제시할 수 있다. 하지만 연구자는 여전히 방향이 수학적으로 타당한지 판단하고, 생성된 코드를 검토하며, 증명 상태가 복잡해질 때 시스템을 이끌어야 한다. 즉 이번 성과는 AI 보조 능력의 발전이지 인간 수학 판단의 대체가 아니다.

형식 증명은 언어 모델에 어려운 시험이다. 모델은 그럴듯하지만 틀린 문장을 만들 수 있지만, Lean은 논리가 맞지 않는 증명을 받아들이지 않는다. 따라서 많은 오류가 자동으로 드러난다. 성공 기준도 달라진다. AI가 우아한 증명 문단을 쓰는지가 아니라, 엄격한 형식 시스템 안에서 검증 가능한 산출물을 꾸준히 완성하도록 도울 수 있는지가 중요하다.

더 넓은 AI 시장에서 이번 연구는 과학과 기술 지식 노동의 미래를 가리킨다. 모델은 번거로운 번역, 탐색, 수리 반복을 맡아 전문가 팀의 속도를 높일 수 있다. 형식 수학, 프로그램 검증, 안전이 중요한 공학은 유창한 텍스트만으로 충분하지 않다. 감사 가능한 추론 체인과 외부 도구가 확인할 수 있는 산출물이 필요하다. 모델이 이런 제약 안에서 더 잘 작동한다면, 전문가 검토를 유지하면서 작업 효율을 높일 수 있다.

Anthropic은 이 작업을 최종 목적지가 아니라 한 단계의 진전으로 제시한다. 대규모 정리 형식화는 여전히 어렵고, 시스템은 인간의 계획과 수정에 의존한다. 그럼에도 이 발표는 최전선 AI 시스템이 단순한 채팅 답변이 아니라 까다로운 환경에서 검증 가능한 결과물을 만들 수 있는지로 평가되고 있음을 보여준다.