수학의 형식화(formalization)는 오랫동안 소수 전문가의 영역이었다. 자연어로 서술된 정리를 Lean이나 Coq 같은 증명 보조 도구가 이해할 수 있는 엄밀한 형식 언어로 옮기고, 다시 그것을 기계가 검증 가능한 방식으로 증명하는 일은 문법 지식과 라이브러리 숙련을 동시에 요구했다. MathCode는 이 과정을 터미널 기반 AI 코딩 에이전트에 통합해, 평범한 문장으로 쓴 수학 문제를 받아 Lean 4 정리로 변환하고 형식 증명까지 시도하도록 만든 도구다. 개발 배경에는 AUTOLEAN 프로젝트의 형식화·증명 파이프라인이 자리하고 있으며, 기본 백엔드로는 codex CLI를 사용한다.
무엇을 하는 도구인가
MathCode의 핵심은 '수학 형식화 엔진을 내장한 코딩 어시스턴트'라는 위치다. 사용자가 자연어로 문제를 입력하면 에이전트가 이를 Lean 4 정리로 자동 변환하고, 지속적으로 살아 있는 Lean REPL 위에서 증명을 반복 시도한다. 각 증명은 하나의 상호작용 세션이 되어, 에이전트가 증명 후보를 작성하고 컴파일 오류를 읽은 뒤 다시 컴파일하는 순환을 거친다. 결과물은 LeanFormalizations/ 디렉터리에 저장되며, 터미널이 아닌 화면을 선호하는 사용자를 위해 ./run webui 명령으로 브라우저 UI도 제공된다. 동작 환경은 macOS(arm64) 또는 Linux(x86_64)로 제한되고, setup.sh가 릴리스 체크아웃과 번들 런타임, Lean 툴체인 다운로드, 사용자 로컬 런처 설치를 처리한다.
실무적으로 가장 눈에 띄는 부분은 속도 처리 방식이다. Lean은 형식 증명의 컴파일 검증이 느린 것으로 잘 알려져 있는데, MathCode는 지속적으로 떠 있는 Lean 언어 서버를 두어 최초 워밍업 한 번 이후에는 컴파일 검사를 약 0.4초 수준으로 낮춘다. 매번 새로 컴파일할 때 약 30초가 걸리던 것과 비교하면, 에이전트가 시행착오를 반복해야 하는 증명 작업에서 이 차이는 단순한 편의가 아니라 반복 루프 자체를 성립시키는 조건에 가깝다.
재사용과 검증을 축으로 삼은 설계
MathCode는 한 번 증명한 결과를 버리지 않는다. 증명에 성공한 모든 정리는 자동으로 이름이 붙고 저장되며 임포트 가능한 형태로 관리되어, 이후 증명기(prover)와 계획기(planner)가 다시 끌어다 쓸 수 있다. 대화 중 등장한 가정 역시 그냥 문맥으로 흘려보내는 것이 아니라 지속적이고 컴파일 검증되며 일관성 검토를 거친 Lean 선언으로 저장된다. 이는 LLM 기반 도구가 흔히 겪는 '맥락이 사라지면 앞서 합의한 전제도 함께 증발하는' 문제를, 형식 언어의 검증 가능성으로 붙잡아 두려는 접근이다.
증명 과정에서 필요한 보조정리는 leansearch.net과 Loogle을 검색해 Mathlib에 이미 검증된 lemma를 찾아 활용하고, 오류 수정에는 구조화된 LSP 진단 정보를 사용한다. 즉 에이전트가 근거 없이 새 명제를 지어내기보다, 표준 라이브러리에 존재하는 검증된 자산을 우선 재사용하도록 유도하는 구조다. 여기에 더해 증명된 정리와 그것이 의존하는 보조정리 사이의 관계를 Obsidian 볼트로 생성해 지식 그래프처럼 시각화한다. 형식 증명의 의존 구조를 사람이 눈으로 따라가며 검토할 수 있게 만든 셈이다.
병렬화 전략과 남는 질문
복잡한 정리에 대해서는 분할 정복 방식을 쓴다. 하나의 큰 정리를 서로 독립적인 하위 목표로 쪼개 병렬로 증명한 뒤 다시 이어 붙이고, 계획기 여러 개를 동시에 돌려 다양한 증명 전략을 만들어낸 다음 증명기가 그중 가장 나은 접근을 고른다. 단일 경로로 막히면 처음부터 다시 시작하는 방식과 달리, 여러 전략을 동시에 탐색해 성공 확률을 높이려는 설계다. 자동 형식화와 증명이 본질적으로 탐색 문제라는 점을 고려하면 합리적인 선택이다.
다만 실무자가 냉정하게 짚어야 할 한계도 분명하다. 공개된 자료는 파이프라인의 구성과 기능을 설명할 뿐, 어떤 난이도의 문제까지 실제로 증명에 성공하는지, 형식화 단계에서 원래 문제의 의미를 얼마나 정확히 보존하는지에 대한 정량적 지표는 제시되어 있지 않다. 형식 증명 도구에서 가장 미묘한 위험은 증명 자체의 오류가 아니라, 자연어 문제를 Lean 정리로 옮기는 과정에서 명제가 원래 의도와 어긋나게 형식화되는 경우다. 그 경우 기계는 '검증된 참'을 돌려주지만 그것이 사용자가 묻고자 한 문제는 아닐 수 있다. 지식 그래프와 일관성 검토는 이런 위험을 사람이 감시할 수 있게 돕는 장치이나, 최종 판단의 책임을 없애 주지는 않는다.
그럼에도 MathCode가 흥미로운 이유는, 코딩 에이전트가 자연어와 형식 검증 사이를 오가는 구체적인 작업 흐름을 하나의 터미널 도구로 묶어냈다는 데 있다. 지속 REPL로 반복 비용을 낮추고, 검증된 결과를 재사용 가능한 자산으로 축적하며, 표준 라이브러리 검색과 LSP 진단으로 수정을 구조화하는 방식은 형식 수학에 국한되지 않는다. 검증 가능한 산출물을 만들어 쌓아 가는 에이전트 설계라는 관점에서, 형식 증명 밖의 개발자에게도 참고할 지점이 있다. 연구에 활용할 경우 프로젝트가 안내한 인용 절차를 따르는 것이 권장된다.