MathCode: 수학 정식화 엔진을 탑재한 AI 코딩 어시스턴트

MathCode는 수학 정식화 엔진을 내장한 터미널 기반 AI 코딩 어시스턴트다. 사용자가 자연어로 수학 문제를 입력하면 이를 Lean 4 정리로 자동 변환하고, 지속적인 Lean REPL과 에이전트 기반 증명 방식을 통해 정식 증명을 시도한다.

주요 기능은 다음과 같다:

• Persistent Lean REPL: 한 번의 워밍업 후 컴파일 체크 시간을 약 30초에서 0.4초로 대폭 단축한다.
• 정리 및 공리 라이브러리: 증명된 정리를 자동 명명하여 저장하고, 대화형 가정을 지속적이고 일관성이 검토된 Lean 선언으로 관리한다.
• Lean LSP 통합: leansearch.net과 Loogle을 통해 Mathlib 렘마를 검색하고, 구조화된 LSP 진단으로 오류를 수정한다.
• Obsidian 정리 그래프: 정리와 렘마 간의 의존 관계를 시각화한 Obsidian 지식 그래프를 생성한다.
• 고도화된 증명 방식: 에이전트가 직접 후보를 작성하고 오류를 읽는 Agent-Mode Proving, 복잡한 정리를 하위 목표로 분해해 병렬로 증명하는 Tree-of-Subgoals, 다양한 전략을 실행하는 Multi-Planner를 지원한다.

이 도구는 AUTOLEAN 프로젝트를 기반으로 하며, macOS(arm64) 및 Linux(x86_64) 환경에서 codex CLI를 통해 사용할 수 있다.