MathCode: Lean 4 형식화를 갖춘 수학적 코딩 에이전트

MathCode는 Lean 4를 사용하여 수학 문제를 형식화하고 증명하는 터미널 기반 AI 코딩 어시스턴트입니다. 직접 Lean 코드를 작성하는 대신, 일반 영어로 문제를 제공하면 정리를 생성하고 증명을 시도하며, 영구 REPL과 재사용 가능한 정리 라이브러리를 제공합니다.

주요 기능

• 영구 Lean REPL: 일회성 워밍업 후 컴파일 검사가 약 30초에서 0.4초로 단축됩니다.
• 정리 라이브러리: 증명된 모든 정리는 자동으로 이름이 지정되고 저장되며 재사용을 위해 가져올 수 있습니다.
• 공리 라이브러리: 대화형 가정을 영구적이고 컴파일 검사된 Lean 선언으로 저장합니다.
• Lean LSP 통합: leansearch.net 및 Loogle에서 검증된 Mathlib 보조 정리를 검색하고, 구조화된 LSP 진단을 사용하여 수정합니다.
• Obsidian 정리 그래프: Obsidian에서 정리와 보조 정리의 시각적 의존성 그래프를 생성합니다.
• 에이전트 모드 증명: 에이전트가 오류를 기반으로 증명 후보를 반복하는 대화형 세션.
• 하위 목표 트리: 복잡한 정리를 독립적인 하위 목표로 분해하고, 병렬로 증명한 다음 결합합니다.
• 멀티 플래너: 다양한 증명 전략을 위해 여러 플래너를 병렬로 실행하며, 프로버가 최상의 접근 방식을 선택합니다.

빠른 시작

macOS(arm64) 또는 Linux(x86_64)와 기본 백엔드용 codex CLI가 필요합니다.

git clone https://github.com/math-ai-org/mathcode.git
cd mathcode
bash setup.sh
codex auth login

다음으로 시도해 보세요:

mathcode -p "짝수의 제곱이 짝수임을 증명"

출력은 LeanFormalizations/에 작성됩니다. 브라우저 UI는 ./run webui로 사용할 수 있습니다.

이 도구는 형식 검증 또는 AI 지원 정리 증명을 다루는 수학자, 연구자 및 개발자를 대상으로 합니다.