MathCode: 수학적 코딩 에이전트

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

주요 기능은 다음과 같다:

• 지속적 Lean REPL: 컴파일 체크 속도를 약 30초에서 0.4초로 단축하여 빠른 피드백을 제공한다.
• 정리 및 공리 라이브러리: 증명된 정리를 자동 명명 및 저장하여 플래너가 재사용할 수 있도록 한다.
• LSP 통합: leansearch.net 및 Loogle을 검색하여 Mathlib 렘마를 활용하고 구조화된 LSP 진단을 사용한다.
• Obsidian 지식 그래프: 정리와 렘마 간의 의존성을 시각화하는 Obsidian 볼트를 생성한다.
• 에이전트 모드 증명: 후보 작성, 오류 읽기, 재컴파일을 수행하는 인터랙티브 세션을 제공한다.
• Tree-of-Subgoals: 복잡한 정리를 독립적인 하위 목표로 분해하여 병렬로 증명한 뒤 다시 결합한다.
• Multi-Planner: 다양한 증명 전략을 위해 여러 플래너를 병렬로 실행하며, 최적의 접근 방식을 선택한다.

이 수학적 정식화 및 증명 파이프라인은 AUTOLEAN 프로젝트를 기반으로 한다.