앤스로픽(Anthropic)의 AI 클로드(Claude)가 수학계의 난제 중 하나인 페르마의 마지막 정리(Fermat's Last Theorem, FLT)를 단 11일 만에 컴퓨터로 완벽하게 검증 가능한 형태로 증명하는 데 성공했습니다. 이는 1637년 피에르 드 페르마(Pierre de Fermat)가 남긴 이래 350년 넘게 수학자들을 괴롭혔던 문제를 AI가 스스로 형식화(formalization)하여 해결한 첫 사례입니다.
페르마의 마지막 정리는 'n이 2보다 큰 정수일 때, aⁿ + bⁿ = cⁿ를 만족하는 양의 정수 a, b, c는 존재하지 않는다'는 내용입니다. 1995년 앤드루 와일즈(Andrew Wiles) 경이 129페이지에 달하는 방대한 증명을 발표했지만, 이를 컴퓨터가 이해할 수 있는 형식으로 변환하는 작업은 수년이 걸릴 것으로 예상되었습니다. 그러나 클로드는 11일 동안 1,300만 줄의 린(Lean) 코드를 작성하고 29,500개의 중간 정리를 증명하며 이 복잡한 과정을 자율적으로 수행했습니다. 이는 인간 수학자들이 수개월 또는 수년에 걸쳐 검증해야 했던 과정을 AI가 단축시킬 수 있음을 보여줍니다.
이번 성과는 수학 연구의 검증 방식에 혁명적인 변화를 가져올 잠재력을 지닙니다. AI가 복잡한 수학적 증명을 자동으로 형식화하고 검증할 수 있게 됨으로써, 새로운 수학적 발견의 신뢰성을 확보하고 검증하는 데 드는 시간과 노력을 획기적으로 줄일 수 있습니다. 이는 수학 지식 체계의 견고성을 높이고, 미래에는 모든 수학적 증명이 컴퓨터로 쉽게 검증될 수 있는 시대를 열어줄 것으로 기대됩니다. 또한, AI가 수학적 추론 능력을 고도화할 수 있음을 입증하며, AI의 활용 범위가 단순 계산을 넘어 복잡한 논리적 사고 영역으로 확장되고 있음을 시사합니다.