AI X/Twitter
NEAR AI Lean 에이전트, PutnamBench 672문제를 111달러에 전부 증명
수학 추론 경쟁의 초점이 정답률에서 검증 가능한 증명의 비용으로 이동했다. NEAR AI 공동창업자 Alex Skidanov는 오픈소스 Lean 에이전트가 PutnamBench 672문제를 111달러에 모두 풀어 차순위 제출보다 비용을 250분의 1로 낮췄다고 밝혔다.
2분 소요 1 조회
태그
#formal-verification
#formal-verification 태그가 달린 기사
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 조회