AI가 에르되시 문제 #728을 거의 자율적으로 풀었다

TL;DR Highlight

AI 도구(Aristotle + LLM)가 미해결 수학 문제 에르되시 #728을 Lean으로 형식 증명하며 수학 연구에서 단순 보조를 넘어 실질적인 증명 파트너로 작동하기 시작했다.

Who Should Read

AI의 실제 추론 능력 한계에 관심 있는 개발자, 형식 증명(Lean, Coq 등) 또는 수학적 AI 응용에 관심 있는 연구자나 엔지니어.

Core Mechanics

에르되시 문제는 헝가리 수학자 폴 에르되시가 남긴 수백 개의 미해결 추측 모음인데, 그 중 #728번 문제가 AI 도구를 활용해 처음으로 Lean 형식 증명으로 완성됐다. 타오의 에르되시 문제 위키에서 Section 1 최초의 '초록(solved)' 표시다.
핵심 도구는 Harmonic이 만든 Aristotle이라는 자동 증명 시스템으로, Lean 코드를 생성하고 검증하는 특화 AI다. 순수 LLM이 아니라 Lean이라는 형식 증명 언어 위에서 AI 탐색을 수행하는 방식이다.
작업 흐름은 이렇다: 사람(타오)이 영어로 비형식적 증명 아이디어를 작성 → Aristotle이 이를 Lean 코드로 변환 시도 → 실패한 부분을 사람이 피드백 → 반복. 완전 자율이 아니라 전문가와 AI의 협력이었다.
Lean 증명의 핵심 강점은 '검증의 확실성'이다. Lean으로 증명이 통과되면 1400줄짜리 코드라도 논리적 오류가 없다는 게 기계적으로 보장된다. 사람이 내용을 이해 못해도 증명이 올바르다는 신뢰가 가능하다.
타오가 강조한 또 다른 포인트는 논문 작성의 빠른 반복이다. 기존에는 논문 초고를 쓰고 리뷰어 피드백에 따라 수정하는 게 몇 달 걸리는 일인데, AI를 활용하면 같은 증명을 다양한 수준과 스타일로 빠르게 재작성할 수 있다고 했다.
Aristotle은 트랜스포머 기반이지만 '언어 모델'이라는 분류와는 다르다. Lean 문법/증명에 특화된 훈련을 받았으며, AlphaFold처럼 도메인 특화 AI의 사례다. 범용 LLM과 달리 수학 형식 언어라는 좁은 도메인에서 훨씬 강한 성능을 낸다.
이 증명은 기존 Mathlib(Lean 수학 라이브러리) 인프라와 가까운 정수론 문제라 AI가 성공할 가능성이 높은 케이스였다. 전문가들은 Mathlib에서 한 단계만 벗어난 문제일수록 AI 자동화가 잘 된다고 지적했다.

Evidence

Harmonic 직원이 직접 댓글을 달아 Aristotle의 동작 방식을 설명했다. '영어 증명이 올바르면 Lean 변환 성공 확률이 높고, Lean 증명이 통과하면 복잡한 증명도 확실히 맞다는 게 우리 접근법의 핵심'이라고 밝혔다. Aristotle을 직접 써볼 수 있는 링크도 공개했다.
'자율적으로 풀었다'는 표현에 회의적인 댓글이 많았다. 타오 같은 세계 최고 수학자가 피드백을 여러 차례 준 것이므로 50:50 협업에 가깝지, AI 자율 해결이라고 보기 어렵다는 반론이 있었다. 제목이 'solved'에서 'more or less solved'로 수정된 것도 이 맥락이다.
1400줄짜리 AI 생성 Lean 코드에 오류가 숨어 있을 수 있다는 우려가 제기됐다. 하지만 Lean 증명의 특성상 코드가 컴파일되면 논리적 오류는 없다는 반박도 함께 나왔다. 문제 statement 자체를 사람이 올바르게 Lean으로 작성했다는 전제가 필요하다는 점도 지적됐다.
'LLM은 그냥 학습 데이터를 짜깁기하는 확률 앵무새'라는 주장이 이제는 유지하기 어렵다는 댓글이 있었다. 2023년에는 LLM이 수학 추론을 못 할 거라고 확신했는데 여기까지 왔다는 회고와 함께, 2026년에 더 많은 미해결 문제가 AI로 풀릴 것이라는 기대가 나왔다.
수학자의 커리어 전망에 대한 질문도 등장했다. 체스에서 딥블루가 카스파로프를 이겼지만 인간 선수 커리어가 끝나지 않았다는 비유를 들며, 수학은 경쟁 스포츠가 아니므로 수학자 직업에 어떤 영향을 줄지 다른 논의가 필요하다는 의견이 있었다.

How to Apply

Lean 또는 Coq 같은 형식 증명 도구를 쓰는 팀이라면 Aristotle(aristotle.harmonic.fun)을 연동해 영어로 증명 아이디어를 작성하고 Lean 코드 초안을 자동 생성하는 파이프라인을 테스트해볼 수 있다.
수학/알고리즘 정확성이 중요한 시스템(금융 계산, 암호화, 컴파일러 검증 등)을 개발 중이라면 LLM이 생성한 증명 아이디어를 Lean 같은 형식 검증 도구로 자동 검증하는 하이브리드 접근을 아키텍처에 포함하는 것을 고려할 수 있다.
논문이나 기술 문서를 작성하는 경우, 타오가 언급한 것처럼 LLM을 활용해 같은 내용을 다양한 수준(입문/전문가/코드 위주 등)으로 빠르게 재작성하는 워크플로우를 실험해볼 수 있다. 특히 리뷰 피드백 반영 시 전체 구조를 재작성해야 할 때 효과적이다.

Terminology

Lean수학 증명을 코드로 작성하면 컴퓨터가 논리적 오류를 검증해주는 형식 증명 언어. 컴파일이 통과되면 증명이 100% 올바르다는 보장이 된다.

MathlibLean으로 작성된 수학 정리들의 라이브러리. 수천 개의 증명이 쌓여 있어 새 증명을 작성할 때 기반으로 활용할 수 있다.

에르되시 문제헝가리 수학자 폴 에르되시가 평생 동안 모아둔 수백 개의 미해결 수학 추측 목록. 상금이 걸린 것도 있고, 아직 대부분이 미해결 상태다.

형식 증명사람이 자연어로 쓰는 수학 증명을 컴퓨터가 검증 가능한 코드 형태로 변환한 것. 모호함이 없고 기계가 오류 여부를 자동 확인한다.

AristotleHarmonic이 개발한 자동 증명 AI. Lean 코드 생성과 탐색에 특화되어 있으며, 범용 LLM과 달리 수학 형식 언어 도메인에 집중한다.