참고팁Hacker News
MathCode: Lean 4 기반 수학적 코딩 에이전트 공개
수학 문제를 Lean 4 정형 증명으로 자동 변환하는 CLI 도구. 정밀한 로직 검증이 필요한 업무에 활용 가능.
요약
MathCode는 사용자가 평문으로 수학 문제를 입력하면 자동으로 Lean 4 정리로 변환하고 형식 증명을 시도하는 터미널 기반 AI 코딩 어시스턴트입니다. 지속적인 Lean REPL, 재사용 가능한 정리 라이브러리, 에이전트 기반 증명 기능을 제공하며, Obsidian 지식 그래프를 통해 정리와 보조 정리 간의 의존성을 시각화합니다. 이 도구는 복잡한 정리를 독립적인 하위 목표로 분해해 병렬로 증명하고 최적의 전략을 선택하며, 영구적인 Lean 언어 서버를 사용하여 컴파일 확인 속도를 0.4초대까지 단축했습니다. 또한 leansearch.net 및 Loogle에서 검증된 Mathlib 보조 정리를 검색하고, 구조화된 LSP 진단을 통해 오류를 수정합니다. 현재 macOS(arm64) 및 Linux(x86_64) 환경을 지원하며 codex CLI를 기본 백엔드로 사용합니다.
AI가 원문을 요약한 내용으로, 부정확할 수 있습니다.
원문 제목 MathCode, Mathematical Coding Agent
원문 보기 ↗