LLM
Mistral, Lean 4 전용 오픈소스 코드 에이전트 Leanstral 공개
Mistral이 2026년 3월 16일 Lean 4 전용 오픈소스 코드 에이전트 Leanstral을 공개했다. 6B active parameters, Apache 2.0 공개, FLTEval 도입, Mistral Vibe와 API 및 가중치 배포가 핵심이다.
1분 소요 38 조회
태그
#lean4
#lean4 태그가 달린 기사
LLM 해커뉴스
Hacker News가 주목한 Leanstral, Mistral의 Lean 4용 open verified coding agent
2026년 3월 16일 Hacker News에서는 Mistral의 Leanstral 공개가 277 points와 49 comments를 기록했다. Lean 4 proof engineering에 맞춘 Apache 2.0 open model과 FLTEval benchmark 결과가 커뮤니티의 관심을 끌었다.
2분 소요 30 조회
AI 레딧
TorchLean: Lean 4에서 신경망 실행·검증 의미를 하나로 묶다
r/MachineLearning에서 주목받은 TorchLean은 PyTorch 스타일 실행 경로와 정형 검증 경로를 Lean 4 안에서 같은 의미 체계로 통합하려는 시도다. Float32 의미론, SSA/DAG IR, IBP·CROWN 계열 검증을 결합해 안전성 검증 파이프라인의 의미 불일치 문제를 줄이는 데 초점을 둔다.
1분 소요 28 조회