Jared Duker Lichtman @jdlichtman는 알려진 수학 전체를 형식 코드로 옮기는 ‘MAP(Mathematics Autoformalization Project)’ 구상을 제시했다. 그는 Claude가 페르마의 마지막 정리를 형식화한 일을 출발점으로, 수학 문헌의 오류를 찾아내고 향후 연구를 뒷받침할 종합 데이터베이스를 만들 수 있다고 주장한다.

알려진 수학 전체를 형식 코드로 번역할 기회가 열렸다. 이는 수학판 인간 게놈 프로젝트나 현대의 AlphaFold에 해당한다.

Lichtman은 9월 4일 Anthropic이 페르마의 마지막 정리를 형식화했다고 소개했다. 페르마는 1637년에 정리를 제시했고, Andrew Wiles와 Richard Taylor가 1995년에 증명했다. 이후 Kevin Buzzard는 사람의 증명을 기계가 검증할 수 있는 코드로 옮기는 프로젝트를 시작했다. Lichtman에 따르면 Buzzard는 5년에 걸쳐 진행할 90만 파운드의 연구비를 확보했지만, 증명에 필요한 20세기 수학 문헌까지 형식화해야 하는 과제가 남아 있었다.

Lichtman은 Claude가 11일 만에 페르마의 마지막 정리와 그에 필요한 문헌을 형식화해 코드 1,300만 줄을 작성했다고 주장한다. 그는 이 성과가 Langlands 프로그램 관련 문헌의 형식화 가능성도 열었다고 본다. Buzzard는 해당 문헌에 미묘한 오류가 있을 수 있다고 우려해 왔다고 Lichtman은 전했다.

형식화 규모의 증가

Lichtman은 수학 형식화 규모가 빠르게 커지고 있다고 설명한다. DeepMind의 IMO 은메달 성과가 최고 기록이던 시기에는 자동 형식화된 수학이 약 400줄 규모였다고 한다. 이후 규모가 커진 사례로 다음을 들었다.

  • 2025년 6월, de Bruijn의 ABC 정리 형식화가 3,500줄에 도달했다.
  • 2025년 9월, 소수 정리의 인간 지원 자동 형식화가 2만 5,000줄을 넘어섰다. 이는 Terry Tao와 Alex Kontorovich가 2024년에 제시한 과제를 완수한 것이다.
  • 2026년 3월, Maryna Viazovska의 필즈상 수상 업적인 구 포장 문제 형식화는 20만 줄에 달했다.
  • 2026년 6월, OpenAI가 Erdős 단위 거리 추측을 자동 형식화한 코드가 100만 줄을 넘었다.

Lichtman은 페르마의 마지막 정리 사례가 1,300만 줄에 이르렀다며, 형식화 규모가 약 다섯 자릿수 증가했다고 설명한다. 그는 코드 줄 수뿐 아니라 증명이 현대 수학의 방대한 내용을 바탕으로 한다는 점과 AI 에이전트의 자율성이 함께 중요하다고 강조했다. 규모 변화를 담은 이미지, 형식화 규모 비교 이미지, 로그 그래프 이미지가 게시물에 포함됐다.

MAP의 목표와 활용 가능성

MAP는 인류가 알고 있는 수학 전체를 포괄하는 형식 데이터베이스를 만들겠다는 구상이다. Lichtman은 이를 알려진 단백질 2억 개를 정리한 AlphaFold에 비유했다. 형식화는 증명의 정확성을 기계적으로 확인하는 것뿐 아니라 문헌의 오류를 드러낼 수 있으며, 그런 오류가 과거에 연구 프로그램 전체를 흔들기도 했다고 그는 주장한다. 이와 관련해 최근 AI 수학 성과에서도 초기 사례가 나타나고 있다고 덧붙였다.

그는 대학원 수학 교육과정의 대수학·해석학·기하학·위상수학·응용수학 핵심 주제부터 교과서와 연구 문헌까지 형식화할 수 있다고 본다. 수학은 지식이 누적되는 분야인 만큼, MAP가 인류 수학의 알려진 영역을 지도처럼 정리할 수 있다는 설명이다.

Lichtman은 Claude의 현재 효율을 기준으로 전체 수학 문헌을 형식화하는 데 약 100억 줄의 코드가 필요하다고 추산했다. 학계와 선도 AI 연구소, 자선단체, 정부가 충분히 협력하고 자금을 지원한다면 다음 1년 안에 이를 달성할 수 있다고 전망했다. 이는 그의 추산과 전망이며, 게시물은 구체적인 실행 계획이나 검증 결과를 제시하지 않는다. 그는 DARPA의 expMath 프로그램을 이끄는 @patshafto와 MAP 개발에 조언한 @ericweinstien에게 감사를 전했다.

Lichtman은 MAP가 검증을 넘어 미래 수학 연구의 기반 시설이 될 수 있다고 주장한다. 현재 화제가 된 AI 생성 수학 결과는 기존 방법을 조합한 성과가 많고, 진정한 독창성이 부족하다는 평가를 받는다고 설명하면서도, 명시적으로 형식화된 코드는 차세대 모델을 훈련할 토대가 될 가능성이 있다고 본다. 먼저 알려진 수학의 영역을 정리해 두면 이후 새로운 수학적 발견을 위한 기반을 마련할 수 있다는 구상이다.

Lichtman은 2019년 James Maynard와 함께 옥스퍼드에서 소수의 수수께끼를 연구하며 박사과정을 시작했다. 그해 Kevin Buzzard의 Lean 강연을 듣고 자연어 수학 증명을 형식 언어로 옮겨 프로그램의 컴파일로 정확성을 확인하는 방식에 관심을 갖게 됐다고 밝혔다. Buzzard는 Tom Hales의 2017년 강연에서 영감을 받아 Lean 프로그래밍에 빠졌으며, 수백 년 된 케플러 추측도 오랜 작업 끝에 형식화됐다고 회고했다. Lichtman은 AI의 발전과 수학 형식화가 자동 형식화라는 형태로 합쳐지고 있으며, 최근 1년간 생성되는 코드의 양과 질이 향상됐다고 평가한다.

그는 게시물 말미에 “상황이 빠르게 변하고 있어 자세한 내용은 추후 전하겠다”고 밝혔다. 원문 게시물은 2026년 9월 8일에 올라왔다. 게시물에는 추가 이미지, 추가 이미지, 답글 링크도 포함돼 있다.