math-ai-org/mathcode

MathCode – AI 기반 Lean 코드 보조 도구

무엇인가요 – MathCode는 Lean 정리 증명 언어에서 형식적 증명을 작성하고 검사하며 검증하는 데 도움을 주는 터미널 기반 AI 코드 에이전트입니다. Lean 도구 체인, 가벼운 웹 UI, 그리고 모델이 Lean과 상호작용할 수 있는 "스킬" 세트를 포함합니다 (선언 검색, 후보 검사, 증명 검증 등).

주요 기능

• 목표 중심의 증명 작성 – 자연어로 목표를 제시(예: "짝수의 제곱은 짝수임을 증명하라")하면 에이전트는 Lean 코드를 반복적으로 생성하고, Lean 도구를 호출하며, 증명을 개선합니다.
• Lean 백엔드 – 인프로세스 Lean REPL, 핀된 하위 프로세스, 또는 외부 Kimina Lean 서버를 사용하여 컴파일 및 검증이 가능합니다.
• 지속적 라이브러리 – 증명된 정리(/theorem-store)와 대화형 공리(/axiomatize)를 버전 관리 가능한 보관소에 저장하여 나중에 재사용할 수 있습니다.
• Obsidian 그래프 내보내기 – 정리 간 의존성에 대한 시각화 지식 그래프를 생성하여 Obsidian에서 열 수 있습니다.
• 웹 UI – 가벼운 브라우저 인터페이스(./run webui)로 로컬 데몬을 실행하고 터미널과 동일한 인터랙티브 세션을 표시합니다.
• 스케줄링 – /loop 10m … 같은 슬래시 명령어로 리마인더나 주기적 검사를 위한 반복 프롬프트를 설정할 수 있습니다.

설치 및 설정

1. 리포지토리 복제 후 bash setup.sh 실행. 스크립트는 다음 작업을 수행합니다:
   • 필요 시 사전 빌드된 런타임 번들(mathcode-vX.Y.Z-<os>-<arch>.tar.gz)을 다운로드합니다.
   • SHA-256 체크섬으로 다운로드를 검증합니다.
   • 사용자 로컬 런처(~/.local/bin/mathcode)를 설치합니다.
   • 번들된 Lean 도구 체인(.local/elan)과 캐시된 Mathlib 스냅샷을 설정합니다.
2. Linux에서는 bubblewrap(bwrap)과 socat가 필요합니다. macOS에서는 번들이 즉시 작동합니다.
3. 기본 OpenAI 기반 모델을 사용하려면 codex CLI를 선택적으로 설치할 수 있습니다.

일반적인 워크플로우

# 인터랙티브 세션 시작
mathcode -p "prove that the square of an even number is even"
# 또는 입력을 파이프로 전달
echo "hello" | mathcode -p

# 웹 UI 실행
./run webui

세션 내에서 슬래시 명령어 사용 가능:

• /goal <budget> <objective> – 토큰 예산을 설정하고 에이전트에게 증명 작업을 요청합니다.
• /theorem-store …, /axiomatize … – 지속적 정리/공리 라이브러리를 관리합니다.
• /obsidian generate – Obsidian 그래프를 갱신합니다.
• /loop … – 반복 프롬프트를 스케줄링합니다.

구성 옵션 (환경 변수)로 시스템을 조정할 수 있습니다. 예를 들어:

• MATHCODE_GOAL_MAX_TOKEN_BUDGET – 목표에 대한 토큰 예산의 상한을 설정합니다.
• MATHCODE_MAX_CHAINED_COMMAND_INPUTS – 에이전트가 수행할 수 있는 중첩된 도구 호출 수를 제한합니다.
• MATHCODE_LEAN_REPL – 인프로세스 REPL을 강제로 사용합니다.
• MATHCODE_KIMINA_SERVER 및 관련 변수 – 외부 Kimina Lean 서버를 지정합니다.

유지보수

• bash setup.sh --status는 바이너리, 체크섬, 번들된 ripgrep의 건강 상태를 확인합니다.
• bash setup.sh --clean은 설치 아티팩트를 제거하지만, 증명 보관소와 Lean 형식화는 유지합니다.

대상 사용자 – Lean을 사용하며 AI 기반 보조 도구를 통해 정리 증명을 가속화하고, Mathlib를 탐색하며 재사용 가능한 형식적 결과 라이브러리를 유지하고자 하는 연구자, 학생, 개발자입니다.

---

위의 모든 세부 정보는 리포지토리의 README에서 직접 인용되었으며, 추가 기능은 추측되지 않았습니다.