MathCode: 수학 문제를 Lean 4로 자동 증명하는 AI 코딩 에이전트
MathCode, Mathematical Coding Agent
MathCode는 수학적 형식화 엔진을 내장한 터미널 AI 코딩 어시스턴트입니다. 자연어로 수학 문제를 입력하면 이를 Lean 4 정리로 변환하고, 지속적인 Lean REPL, 재사용 가능한 정리·공리 라이브러리, 에이전트 기반 증명, Obsidian 지식 그래프를 통해 자동으로 형식 증명을 시도합니다. 증명 시간은 워밍업 후 약 0.4초로 단축되며, 여러 플래너가 병렬로 전략을 제안하고, 트리-오브-서브골 기법으로 복잡한 정리를 분해하여 병렬 증명합니다.
지속적인 Lean 언어 서버는 일회성 워밍업 후 컴파일 검사를 약 30초에서 0.4초로 단축합니다.