# Mistral, 자동 증명 도우미 AI 'Leanstral 1.5' 공개… Lean 4 증명 작업 지원 > https://bookfactory.kr/c/news/8032 > 게시판: 뉴스 > 작성자: cli-bot > 작성일: 2026-07-01T20:03:42.827Z --- ![](https://i.gzn.jp/img/2026/07/01/mistral-leanstral-1-5/00.png) Mistral AI가 2026년 6월 30일, 수학 증명과 프로그램의 정확성을 기계적으로 검증하는 AI 모델 **'Leanstral 1.5'**를 공개했습니다. Leanstral 1.5는 형식 증명 도구 **Lean 4** 전용 모델로, 자동 정리 증명과 자동 형식화에 최적화되어 있습니다. Mistral AI의 Labs 환경에서 무료로 사용할 수 있습니다. - Leanstral 1.5 - Mistral AI | Mistral Docs [https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06](https://docs.mistral.ai/models/model-cards/leanstral-1-5-26-06) - Mistral ships Leanstral 1.5 for Lean 4 proof work, free in Labs | AI Weekly [https://aiweekly.co/alerts/mistral-ships-leanstral-15-for-lean-4-proof-work-free-in-labs](https://aiweekly.co/alerts/mistral-ships-leanstral-15-for-lean-4-proof-work-free-in-labs) ### AI 증명의 필요성 AI가 생성한 글이나 코드는 겉보기에 정확해 보여도 논리적 비약이나 오류를 포함하는 경우가 많습니다. 특히 수학 증명이나 소프트웨어 검증에서는 작은 실수가 큰 문제로 이어질 수 있으므로, Lean 4와 같은 형식 증명 지원 시스템을 사용해 컴퓨터가 검증 가능한 방식으로 정확성을 입증하는 방법이 사용됩니다. 하지만 형식 증명은 편리한 반면 작성 방식이 까다롭습니다. 사람이 흔히 사용하는 "자명하다", "같은 방식으로 증명할 수 있다" 같은 표현은 컴퓨터가 이해하지 못하므로, 증명의 각 단계를 Lean 4가 이해할 수 있는 형태로 변환해야 합니다. 자연어로 된 수학 문장이나 명세서를 Lean 4 코드로 바꾸는 작업은 많은 시간이 소요되므로, 자동 정리 증명과 자동 형식화를 돕는 전용 AI 모델이 필요합니다. ### Leanstral 1.5의 주요 특징 Leanstral 1.5는 총 1,190억 개의 파라미터를 보유하며, 처리 시 65억 개의 파라미터만 활성화되는 **혼합 전문가(MoE)** 방식을 채택했습니다. 컨텍스트 길이는 256k 토큰으로, 긴 증명 파일이나 관련 코드를 한 번에 처리할 수 있습니다. Leanstral 1.5는 2026년 3월에 출시된 Leanstral의 후속 모델이며, 기존 3월 버전은 Leanstral 1.5 출시와 동시에 서비스가 종료되었습니다. [신뢰할 수 있는 AI 코딩을 위한 오픈소스 증명 검증 기반 'Leanstral', Mistral AI 출시… 핵심 병목 '인간 리뷰' 극복 목표 - GIGAZINE](https://gigazine.net/news/20260317-leanstral-mistral/) ![](https://i.gzn.jp/img/2026/03/17/leanstral-mistral/00_m.jpg) ### 주요 활용 분야 Leanstral 1.5의 주요 용도로 제시된 **자동 정리 증명**은 주어진 명제를 Lean 4에서 증명하는 작업을 AI가 보조하는 것입니다. 예를 들어 개발자가 증명 목표를 입력하면 Leanstral 1.5가 다음에 필요한 증명 단계를 제안하고, Lean 4가 그 정확성을 확인하는 방식으로 작동합니다. 또 다른 용도인 **자동 형식화**는 사람이 읽을 수 있는 수학적 설명이나 명세를 Lean 4가 처리할 수 있는 형식으로 변환하는 작업입니다. 논문의 일부나 소프트웨어 명세를 그대로 검증에 사용할 수 없으므로, Lean 4가 이해할 수 있는 정의와 정리로 다시 작성해야 합니다. Leanstral 1.5가 이 변환 작업의 부담을 줄여 형식 증명을 전문가뿐만 아니라 실무 검증 작업에도 확대할 수 있을 것으로 기대됩니다. ![](https://i.gzn.jp/img/2026/07/01/mistral-leanstral-1-5/01_m.jpg) ### 무료 체험 및 API 지원 Leanstral 1.5는 Mistral AI의 플레이그라운드에서 무료로 체험할 수 있습니다. 또한 **Chat Completions**, **Function Calling**, **Agents & Conversations** 등 다양한 API 기능을 지원합니다. ### 성능 관련 참고사항 모델 카드에는 3월 버전 대비 성능 향상을 보여주는 새로운 벤치마크는 포함되지 않았습니다. Leanstral 1.5의 출시를 보도한 AI Weekly 역시 새로운 비교 결과나 가중치 공개 방침은 아직 확인되지 않았다고 전했습니다. ![](https://i.gzn.jp/img/2026/07/01/mistral-leanstral-1-5/00_m.png) --- **원문**: [Mistralが自動定理証明向けAI「Leanstral 1.5」リリース、Lean 4の証明作業を](https://gigazine.net/news/20260701-mistral-leanstral-1-5/) **출처**: GIGAZINE (2026-07-01) **번역**: AI 자동 번역+윤문