MathCode: 수학 문제를 Lean 4로 형식화·증명하는 터미널 코딩 에이전트

Who Should Read

증명 검증기(Lean)를 에이전트 루프에 붙여 결과를 기계적으로 검증하고 싶은 에이전트 개발자

Core Mechanics

• 자연어 문제를 Lean 4 정리로 변환
  • 평이한 말로 문제를 주면 Lean 4 theorem으로 바꾼다.
  • 이어서 형식 증명(컴퓨터가 검증하는 증명)을 시도한다.
• Lean 검증 통과만 완료로 인정
  • 마지막에 새로 돌리는 strict 검증이 선언 하나를 확인한다.
  • 검증 성공 인증서가 있어야 증명 완료로 센다.
• 에이전트가 증명 방향을 직접 결정
  • 후보 작성, 목표·진단 확인, 다음 시도 선택을 에이전트가 한다.
  • 서브골·보조 보조정리·분기·마일스톤은 선택 기법일 뿐 강제 컨트롤러가 아니다.
• Lean 환경 연동 기능이 많다
  • 지속되는 Lean REPL과 Lean LSP 진단으로 오류를 고친다.
  • leansearch.net과 Loogle에서 검증된 Mathlib 보조정리를 검색한다.
• 재사용 라이브러리와 지식 그래프 제공
  • 정리 라이브러리와 공리 라이브러리에 컴파일 검증된 선언을 저장한다.
  • 정리와 보조정리의 의존 관계를 Obsidian 그래프로 보여 준다.

Community Reactions

• Lean 형식화가 맞는지가 핵심이라는 의견
  • 부정확한 평이한 문장이 Lean으로 올바르게 옮겨지는지 확인하는 부분이 까다롭다는 댓글이 있었다.
• AUTOLEAN 래퍼냐는 질문
  • AUTOLEAN 프로젝트(T3S1AMAX/autolean)를 감싼 것이냐고 묻는 댓글이 있었다.
• 라이선스 표기가 없다는 지적
  • 라이선스 조건이 보이지 않아 상업 환경에서는 쓸 수 없다는 댓글이 있었다.
• 예시가 먼저 나와야 한다는 의견
  • 퀵스타트·기능 목록보다 예시가 먼저 있어야 무엇인지 알겠다는 댓글이 있었다.

How to Apply

• 예제 문제 하나로 설치·실행해 보기
  • 시간이 있을 때 --without-lean 옵션으로 가볍게 설치한다.
  • mathcode -p "prove that the square of an even number is even"를 실행해 결과를 확인한다.
• 에이전트 완료 판정을 외부 검증기로 바꾸기
  • 에이전트 작업의 완료 조건을 모델 자체 판단이 아니라 컴파일러·테스트 통과로 둔다.
  • 마지막 검증은 캐시 없이 새로 실행하도록 구성한다.
• 검증 가능한 영역에 같은 구조 적용 검토하기
  • 형식 검증이 가능한 작업에서 후보 작성, 진단 확인, 재시도 순환으로 에이전트를 만든다.
  • 방법은 강제하지 말고 선택 가능한 기법으로 제공한다.
• 라이선스를 먼저 확인하기
  • 사내 사용 전에 저장소에서 라이선스 파일 유무를 확인한다.
  • 없으면 사용 전에 저자에게 문의한다.

Try It

# 터미널에 붙여넣기 (원문 Quick Start 기반, macOS arm64 또는 Linux x86_64 AVX2, codex CLI 필요)

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

# 실행
mathcode -p "prove that the square of an even number is even"

# 이어서 해 볼 것: 웹 UI는 ./run webui, 전체 Lean 도구체인은 --with-lean

Terminology

관련 논문

• 같은 시뮬레이션, 다른 근거: 도구 출력을 파일로 넘기면 LLM 에이전트 정확도가 어디서 깎이나

  긴 툴 출력을 파일로 넘기자 GPT-5.1은 정확도 11.3%p 하락, 정식 출력 지정하니 회복

• 가짜 뉴스가 진짜 폭락을: LLM 트레이딩 에이전트 대상 정보 주입 공격

  가짜 헤드라인 한 줄로 LLM 트레이딩 에이전트 62%를 조종했다(프롬프트 주입은 14%)

• Harness Engineering 101: LLM은 뇌, harness는 몸

  에이전트는 JSON 배열을 관리하는 루프이고, 16개 챕터로 직접 만들어 본다

• Harness²: 에이전트 harness를 스스로 고쳐 쓰는 재귀 최적화 프레임워크

  모델은 고정하고 harness를 재귀로 고쳤더니 벤치마크 점수가 최대 11.8%p 올랐다

• 해고된 Savannah 경찰관, ICE 요원 남편에게 Flock 계정 공유

  경찰관이 Flock 계정을 남편(ICE 요원)에게 공유했고, 감사에서 983건 검색이 드러나 해고됐다

• tmux와 Claude Code: 세션, send-keys, 그리고 한계선

  tmux로 Claude Code 여러 개를 돌리면 편하지만 에이전트 4개쯤에서 한계가 온다

• Hybrid Reasoning Agents: 잠재 공간에서 생각하고 텍스트로 행동하는 LLM 에이전트

  잠재 공간 추론과 텍스트 도구 호출을 섞었더니 성능 10.4%↑, 토큰 최대 54.7%↓

Related Resources

• https://math-ai.org/mathcode/
• https://math-ai-org.github.io/mathcode/
• https://github.com/math-ai-org/mathcode
• https://github.com/T3S1AMAX/autolean
• https://theoremdb.org