자연어로 수학 증명을 자동화하는 AI 에이전트 MathCode의 등장 (math-ai-org.github.io)

한줄 요약

자연어 수학 문제 → Lean 4 정형 증명 자동화, 컴파일 검증까지 ~0.4초.

무엇이 달라지나?

MathCode는 터미널 기반 AI 코딩 어시스턴트다. 핵심은 내장된 수학 형식화 엔진에 있다. 사용자가 평문으로 수학 문제를 입력하면, 이를 자동으로 Lean 4 정리(theorem)로 변환하고 형식적 증명(formal proof)을 시도한다.

기존에 Lean 같은 정리 증명 언어를 사용하려면 언어 자체에 대한 깊은 이해가 선행돼야 했다. MathCode는 이 진입 장벽을 자연어 인터페이스로 낮춘다. mathcode -p "prove that the square of an even number is even" 같은 명령 한 줄로 증명 프로세스 전체가 시작된다.

기술적으로 눈여겨볼 점은 몇 가지다.

컴파일 속도: 지속형 Lean 언어 서버(Persistent Lean REPL)를 통해 컴파일 체크를 최초 워밍업 이후 약 0.4초 수준으로 수행한다. 기존 방식 대비 현저히 빠른 피드백 루프를 제공한다.

정리 라이브러리 누적: 증명된 정리는 자동으로 명명되고 저장되며 이후 증명에 재사용 가능하다. 공리(axiom) 역시 컴파일 검증과 일관성 검토를 거쳐 영구 저장된다.

병렬 증명 전략: Tree-of-Subgoals 방식으로 복잡한 정리를 독립적인 하위 목표로 분해하고 병렬 처리한 뒤 결합한다. 복수의 플래너를 동시에 실행하는 Multi-Planner 구조도 지원한다.

지식 그래프 시각화: 증명 결과를 Obsidian 볼트 형태로 내보내 정리와 보조 정리(lemma) 간의 의존 관계를 그래프로 시각화할 수 있다.

또한 Lean LSP 통합을 통해 leansearch.net과 Loogle에서 검증된 Mathlib 보조 정리를 검색하고, 구조화된 진단 정보를 활용해 증명 오류를 자동 수정하는 흐름도 갖추고 있다.

실무에서 어떤 의미인가?

수학적 엄밀성이 요구되는 소프트웨어 개발 분야에서 이 도구의 파급력은 적지 않다. 암호학, 금융 알고리즘, 형식 검증이 필요한 시스템 소프트웨어 등의 영역에서 개발자가 수작업으로 수행하던 증명 과정의 일부를 자동화할 수 있게 된다.

개발 외주나 앱 개발, 웹 개발 프로젝트에서도 이런 흐름은 무관하지 않다. 수학적 알고리즘의 정확성 검증이나 로직 오류 탐지에 형식 증명 도구를 접목하는 시도가 늘고 있기 때문이다. 지금까지는 전문 지식 없이 Lean을 쓰는 것 자체가 벽이었는데, MathCode는 그 벽을 상당히 낮춘다.

다만 이 도구가 수학 전문가를 대체한다는 의미는 아니다. 에이전트가 증명 후보를 작성하고, 오류를 읽고, 재컴파일하는 반복 과정을 자율적으로 수행하지만, 복잡한 수학적 판단이나 증명 전략의 설계는 여전히 인간의 영역이다. 자동화가 가능한 반복 작업을 걷어내고 핵심 판단에 집중할 수 있게 해주는 도구로 이해하는 것이 정확하다.

도입 전 체크포인트

MathCode는 현재 macOS(arm64) 또는 Linux(x86_64) 환경을 요구하며, 기본 백엔드로 codex CLI가 필요하다. Windows는 공식 지원 대상이 아니다.

설치는 GitHub 저장소를 클론한 뒤 setup.sh를 실행하는 방식이며, 런타임과 Lean 툴체인이 함께 다운로드된다. 브라우저 UI도 제공되므로 터미널이 익숙하지 않은 팀원도 ./run webui 명령으로 웹 인터페이스를 활용할 수 있다.

증명 결과물은 LeanFormalizations/ 디렉터리에 저장되므로, 팀 단위로 사용할 경우 해당 디렉터리의 버전 관리 방침을 미리 정해두는 것이 좋다. 내부 수학 형식화 및 증명 파이프라인은 AUTOLEAN 프로젝트를 기반으로 한다.

연구 목적으로 활용할 경우 공식 인용 정보가 제공되므로, 논문이나 기술 보고서에서 참조할 때 활용할 수 있다.