AI가 페르마의 마지막 정리를 다시 풀었다고요? 진짜 혁신은 따로 있습니다

앤트로픽이 페르마의 마지막 정리를 Lean 4로 형식화하는 작업을 시작했습니다. 얼핏 들으면 AI가 수백 년 묵은 난제를 다시 푼 듯하지만, 실제로는 수학의 신뢰 체계를 코드로 다시 만드는 일에 가깝습니다.

페르마의 마지막 정리를 다시 푸는 것은 아닙니다

페르마의 마지막 정리의 내용은 간단합니다. 정수 (n)이 2보다 클 때 (a^n+b^n=c^n)을 만족하는 양의 정수 (a), (b), (c)는 존재하지 않는다는 것입니다.

피에르 드 페르마가 이 명제를 남긴 때는 1637년 무렵입니다. 앤드루 와일스는 1993년에 증명을 발표했지만 결함이 발견됐습니다. 이후 리처드 테일러와 함께 문제를 수정했고, 완성된 논문은 1995년에 출판됐습니다.

이번 작업은 새로운 해답을 찾으려는 시도가 아닙니다. 이미 수학계가 인정한 증명을 Lean 4가 한 단계씩 확인할 수 있는 형태로 옮기는 것이 목표입니다.

따라서 표현도 정확히 해야 합니다. “앤트로픽의 AI가 페르마의 마지막 정리를 증명했다”는 말은 사실과 다릅니다. 핵심은 인간의 증명을 기계가 검증할 수 있도록 형식화한다는 데 있습니다.

논문을 코드로 옮기는 일이 어려운 이유

수학 논문은 많은 내용을 생략합니다. 전문가라면 당연히 알 것이라 보는 정의와 계산은 한두 문장으로 건너뜁니다. “명백하다”거나 “같은 방식으로 얻는다”는 표현도 자주 등장합니다.

Lean 4에서는 이런 생략이 통하지 않습니다. 어떤 정의를 썼고 어느 정리를 적용했는지, 필요한 조건을 모두 충족했는지 정확히 적어야 합니다. 코드 한 줄에 필요한 전제가 하나라도 빠지면 검증은 그 자리에서 멈춥니다.

와일스의 증명은 특히 까다롭습니다. 페르마가 남긴 식을 곧바로 다루는 방식이 아니기 때문입니다. 타원곡선, 모듈러 형식, 갈루아 표현 같은 현대 정수론의 방대한 이론을 거쳐 결론에 도달합니다.

집짓기에 비유하면 이해가 쉽습니다. 마지막에 올릴 지붕만 Lean 4로 만든다고 끝날 일이 아닙니다. 지붕을 받칠 벽과 기둥은 물론, 필요한 자재의 규격까지 먼저 정해야 합니다. 증명 하나를 형식화하는 동안 관련 수학 라이브러리 전체도 함께 커질 수밖에 없는 이유입니다.

수학을 ‘푸는 AI’와 증명을 ‘검증하는 AI’

새로운 문제를 푸는 AI는 다음 단계를 제안합니다. 새로운 보조정리를 떠올리기도 하고, 기존 정리들을 예상하지 못한 방식으로 연결하기도 합니다. 이때는 창의적인 추론과 탐색이 필요합니다.

형식화 작업에서 AI가 하는 일은 조금 다릅니다. 자연어로 적힌 논증을 Lean 코드 초안으로 옮기고 필요한 보조정리를 찾습니다. 타입 오류를 고치거나 빠진 전제를 추적하는 작업도 도울 수 있습니다.

중요한 차이는 누가 마지막 판단을 내리느냐에 있습니다. 언어 모델은 그럴듯해 보이지만 틀린 코드를 만들 수 있습니다. 반면 Lean 4에서 검증을 담당하는 작은 핵심부인 커널은 제출된 증명 항목이 규칙에 맞는지만 기계적으로 판단합니다.

비유하자면 AI는 답안을 작성하는 쪽이고, Lean 4는 계산 과정까지 꼼꼼히 살피는 채점자입니다. AI가 아무리 자신 있게 답을 내놓아도 커널을 통과하지 못하면 증명으로 인정받을 수 없습니다.

형식화가 인간의 증명을 더 선명하게 만듭니다

형식 증명의 장점은 오류를 찾는 데만 있지 않습니다. 논문 속에 숨어 있던 의존 관계도 드러냅니다. 어떤 정리가 어느 가정을 바탕으로 하는지 코드를 통해 추적할 수 있습니다.

재사용하기도 쉬워집니다. 한 번 검증된 정의와 보조정리는 다음 연구에 필요한 부품이 됩니다. 개발자가 검증된 오픈소스 라이브러리를 가져다 쓰듯, 수학자도 신뢰할 수 있는 정리를 조합해 더 큰 결과를 만들 수 있습니다.

그렇다고 형식화만으로 수학적 이해가 저절로 생기는 것은 아닙니다. Lean이 “맞다”고 판정한 코드가 곧 사람에게 좋은 설명이 되는 것도 아닙니다. 검증 가능한 증명과 이해하기 좋은 증명은 서로 다른 결과물입니다.

최근 30일 동안 확인할 수 있는 공개 커뮤니티 논의는 매우 제한적이었습니다. 그래서 온라인 반응의 규모나 분위기를 추천수와 댓글수만 보고 단정하기는 어렵습니다. 다만 “AI가 난제를 해결했다”는 해석과 “기존 증명을 코드로 번역했을 뿐”이라는 해석 사이에 벌어진 간극은 이번 프로젝트를 이해하는 중요한 단서입니다.

진짜 변화는 수학의 생산 방식입니다

이번 도전의 성패를 페르마의 마지막 정리 하나만 놓고 평가하면 핵심을 놓치게 됩니다. 더 큰 변화는 인간이 아이디어를 내면 AI가 형식화를 돕고, Lean이 그 결과를 검증하는 협업 방식에 있습니다.

소프트웨어 개발에 테스트와 자동 검증이 자리 잡았듯, 수학에서도 비슷한 변화가 일어나고 있습니다. 앞으로 눈여겨볼 것은 AI가 인간보다 먼저 답을 찾는지만이 아닙니다. 우리가 믿는 증명을 어디까지 검증 가능한 지식으로 바꿀 수 있을지가 더 중요한 질문입니다.