AI 요약
MathCode는 수학적 형식화 엔진이 내장된 터미널 기반 AI 코딩 에이전트로, 자연어 수학 문제를 Lean 4 정리로 자동 변환하고 형식 증명을 시도한다. 영구 Lean REPL, 정리·공리 라이브러리, 에이전트 기반 증명, Obsidian 지식 그래프를 제공하며, macOS(arm64)와 Linux(x86_64)를 지원한다. 복잡한 정리를 독립적인 하위 목표로 분해해 병렬 증명하는 Tree-of-Subgoals 기능과 다중 플래너 병렬 실행 기능을 갖췄다. AUTOLEAN 프로젝트를 기반으로 수학 형식화 및 증명 파이프라인을 구축했다.
핵심 포인트
- 자연어 수학 문제 → Lean 4 정리 변환 → 형식 증명 자동화
- 영구 Lean REPL로 컴파일 검사 시간을 약 30초에서 0.4초로 단축
- 증명된 모든 정리는 자동 저장·재사용 가능하며 Obsidian 볼트로 지식 그래프 시각화
- Tree-of-Subgoals로 복잡한 정리를 병렬 증명 후 통합, 다중 플래너로 다양한 증명 전략 병렬 실행
향후 전망
- 수학 연구 및 교육 분야에서 AI 기반 형식 증명 자동화의 실용적 도구로 자리잡을 가능성
- Lean 생태계와 통합을 통해 검증 가능한 수학 코딩 에이전트 표준으로 발전할 여지
출처:hackernews