Leanstral: Lean 4 공식 증명을 위한 오픈소스 코딩 에이전트

TL;DR Highlight

Mistral이 Apache 2.0으로 공개한 Lean 4 정형 증명 에이전트 Leanstral은 Claude Sonnet 대비 15분의 1 비용으로 동등하거나 우수한 성능을 달성한다.

Who Should Read

미션 크리티컬한 소프트웨어나 수학 연구에 AI 코드 생성을 적용하면서 정확성 검증이 병목인 개발자나 연구자. Lean 4 또는 형식 검증(formal verification)에 관심 있는 수학/CS 연구자.

Core Mechanics

AI가 생성한 코드를 사람이 직접 검토하는 것이 엔지니어링 속도의 가장 큰 병목인데, Leanstral은 코드 작성과 동시에 수학적으로 엄밀한 명세(specification)를 증명해주는 에이전트로 이 문제를 해결하려 한다.
Lean 4는 수학 증명 보조 도구(proof assistant)로, 퍼펙토이드 공간 같은 복잡한 수학 구조와 Rust 코드 속성 같은 소프트웨어 명세를 모두 표현할 수 있다. Leanstral은 이 Lean 4 전용으로 설계된 최초의 오픈소스 코드 에이전트다.
아키텍처는 MoE(Mixture of Experts, 여러 전문가 모델 중 필요한 것만 활성화하는 구조) 기반으로 총 120B 파라미터이지만 실제 추론 시 활성화되는 파라미터는 6B뿐이라 효율이 높다. 가중치는 Apache 2.0 라이선스로 완전 공개된다.
평가 기준으로 FLTEval이라는 새 벤치마크를 함께 공개했다. 기존 경쟁 수학 문제 풀기 위주의 평가에서 벗어나, 실제 FLT(Fermat's Last Theorem) 프로젝트 PR에서 공식 증명을 완성하고 새로운 수학 개념을 올바르게 정의하는 현실적 작업을 평가한다.
오픈소스 모델 대비 효율이 두드러진다. GLM5-744B-A40B와 Kimi-K2.5-1T-32B는 FLTEval에서 각각 16.6, 20.1에 그치는데, Leanstral은 단 1회 패스(pass@1)로 이를 넘어선다. 가장 강력한 OSS 경쟁자인 Qwen3.5-397B-A17B가 4회 패스로 25.4를 달성할 때, Leanstral은 2회 패스(pass@2)만으로 26.3을 달성한다.
Claude 패밀리와의 비교에서 비용 효율이 압도적이다. Leanstral pass@2(비용 $36)가 Claude Sonnet($549)보다 2.6점 높고, pass@16($290)은 Sonnet보다 8점 높다. Claude Opus 4.6은 39.6으로 여전히 1위지만 비용이 $1,650으로 Leanstral의 92배다.
lean-lsp-mcp(Lean Language Server Protocol을 MCP로 래핑한 도구)와 함께 사용할 때 성능이 최대로 발휘되도록 학습했으며, Mistral Vibe를 scaffold로 사용해 임의의 MCP를 붙일 수 있다.
실전 사례로, Lean 4.29.0-rc6에서 갑자기 컴파일이 안 되는 코드 문제를 Leanstral이 해결했다. `def`로 정의된 타입 별칭이 `rw` 전술의 패턴 매칭을 막는 definitional equality 문제를 스스로 진단하고, `def`를 `abbrev`로 바꾸는 수정안을 제시했다.

Evidence

형식 검증이 AI 코딩의 구조적 해법이라는 의견이 있었다. 검증 스위트는 시간이 지날수록 '코드가 어떻게 동작해야 하는지'를 코드로 표현한 문서로 쌓이는데, 코드가 올바를 때는 컨텍스트 토큰을 전혀 소모하지 않는 실행 가능한 문서라는 점에서 마크다운 명세보다 강력하다는 주장이 있었다.
형식 검증이 AI 코드의 근본 문제를 해결하지 못한다는 반론도 있었다. 함수가 명세에 맞는지는 증명할 수 있지만, '데이터베이스 자격증명을 하드코딩하지 말 것', 'CORS를 열어두지 말 것', '관리자 라우트에 인증을 달 것' 같은 아무도 명세에 적지 않는 보안 요건은 형식 검증 범위 밖이라는 지적이 있었다.
비용 대비 성능 해석에 의문을 제기하는 댓글이 있었다. Leanstral이 Haiku보다 10배 싸지만 성능도 낮은데, 정확성이 중요한 작업에서 '싸지만 못하다'는 게 의미 있냐는 의문이었다. 반면 Opus가 이 벤치마크에서 그다지 좋지 않다는 점은 희망적으로 봤고, Leanstral을 스케일업하면 Opus를 이길 가능성이 있다는 해석도 있었다.
실용성에 대한 회의적인 시각도 있었다. 소프트웨어 현장에서 property-based test조차 도입하기 힘든데, 형식 증명은 훨씬 더 멀다는 경험담이 있었다. 또한 AI가 생성한 증명은 읽기 어렵고 우아하지 않을 것이며, 증명이 올바른 것을 명세하고 있는지 사람이 검토해야 하는 요건은 여전히 사라지지 않는다는 지적이 있었다.
Mistral의 전략적 방향에 대한 비판도 있었다. 주류가 아닌 학문적 영역에 집중하고 프런티어 모델에서 뒤처지고 있다는 의견이 있었다. 반면 모델 alignment 다양성 측면에서 Mistral 같은 회사가 존재하는 것 자체가 중요하다는 반론도 있었다. 한편, 가중치가 실제로 Apache 2.0임을 확인하며 진짜 오픈소스라고 긍정적으로 평가한 댓글도 있었다.

How to Apply

Lean 4 기반 수학 라이브러리나 정형 검증 프로젝트에서 반복적인 증명 작성 작업이 병목인 경우, Leanstral을 lean-lsp-mcp와 함께 에이전트 모드로 연결하면 pass@2~4 수준에서 Claude Sonnet 대비 15분의 1 비용으로 비슷하거나 더 나은 증명 완성률을 얻을 수 있다.
Lean 버전 업그레이드로 인해 기존 코드가 갑자기 컴파일 안 되는 상황이 생겼을 때, Leanstral에게 실패 환경을 재현하는 테스트 코드를 먼저 작성하게 하고 원인을 진단하게 하면 전문가 없이도 breaking change를 추적하는 데 활용할 수 있다.
미션 크리티컬 소프트웨어에 AI 코드 생성을 도입하면서 정확성 보장이 필요한 경우, Lean 4로 핵심 비즈니스 로직의 명세를 작성하고 Leanstral로 구현이 명세를 만족함을 증명하는 파이프라인을 구축하면 사람이 직접 검토하는 병목을 줄일 수 있다. 다만 보안 관련 요건은 별도로 명세에 포함해야 검증이 가능하다.
현재 Mistral Vibe와 무료 API 엔드포인트를 통해 접근 가능하므로, Lean 4를 처음 접하는 경우 비용 부담 없이 실험해볼 수 있다. 여러 모델을 번갈아 사용하는 앙상블 패스(예: Leanstral → Qwen → Leanstral 순서)가 동일 모델 반복 패스보다 성능이 좋을지 실험해보는 것도 커뮤니티에서 제안된 아이디어다.

Terminology

Lean 4수학 정리나 소프트웨어 명세를 코드로 작성하고 컴퓨터가 그 증명을 자동으로 검증해주는 도구. 코드가 '왜 맞는지'를 수학적으로 증명할 수 있게 해준다.

formal verification프로그램이 주어진 명세를 100% 만족함을 수학적으로 증명하는 기법. 테스트는 특정 입력에서만 확인하지만, 형식 검증은 모든 가능한 입력에 대해 보장한다.

MoE (Mixture of Experts)모델 내부에 여러 '전문가' 서브네트워크를 두고 입력마다 일부만 활성화하는 아키텍처. 파라미터 수는 많지만 실제 계산량은 적어 비용 효율이 높다.

MCP (Model Context Protocol)AI 에이전트가 외부 도구(파일 시스템, 언어 서버, API 등)와 표준화된 방식으로 연동하기 위한 프로토콜. USB 포트처럼 다양한 도구를 꽂아 쓸 수 있게 해준다.

pass@k동일한 문제를 k번 시도해서 그 중 하나라도 맞으면 성공으로 보는 평가 방식. pass@2는 2번 시도 중 1번이라도 통과하면 됨을 의미한다.

FLTEval페르마의 마지막 정리(Fermat's Last Theorem) 형식화 프로젝트의 실제 PR을 기반으로 만든 벤치마크. 경쟁 수학 문제가 아닌 실제 대규모 증명 저장소에서의 성능을 측정한다.