AI, 페르마의 마지막 정리를 역대 최대 규모의 Lean 증명으로 구현

페르마의 마지막 정리가 처음으로 컴퓨터가 검증할 수 있는 코드로 옮겨졌다. 단 11일 만에 1,300만 줄에 달하는 형식 증명이 만들어졌다. AI 에이전트 집단은 수학적 논리를 검증하도록 설계된 프로그래밍 언어 Lean에서 작업을 완성하는 데 필요한 약 2만 9,500개의 중간 정리를 개발했다.

이번 성과는 앤드루 와일스와 리처드 테일러가 1990년대에 완성한 인간의 증명을 대체하거나 확장한 것이 아니다. 이미 확립된 논증을 컴퓨터가 단계별로 검증할 수 있는 형태로 변환한 것이다. 이 정리는 n이 2보다 클 때 aⁿ + bⁿ = cⁿ을 만족하는 양의 정수가 없다는 내용이다.

인간 전문가들은 때때로 큰 방향을 제시했다. 에이전트들은 처음에는 작업 조율에 어려움을 겪었지만, 완료한 작업을 추적하고 다음에 무엇을 다룰지 선택하도록 돕는 협업 도구 Prove2Me를 사용한 뒤 성공했다. 수학자 케빈 버저드는 생성된 코드를 컴파일하고 Lean의 표준 검사를 실행한 결과, 이 코드가 필요한 수학적 내용을 실제로 전개한다고 결론 내렸다.

이번 형식화의 규모는 Lean 수학의 주요 공유 라이브러리인 Mathlib의 5배가 넘는다. 이는 AI가 머지않아 수학 문헌의 상당 부분을 검증 가능한 코드로 변환하는 데 도움을 줄 수 있음을 시사한다. 다만 이렇게 거대한 결과물을 검토하고 사람이 이해할 수 있도록 만드는 일은 여전히 상당한 과제다.