setsosie/lms：测量弱 LLM 智能体群体能否积累 Lean 验证数学的开源项目

GitHub 项目 setsosie/lms 提出测量指标 CVFN（每个验证为忠实且新颖的陈述的成本），用六道门槛检验弱 LLM 智能体群体能否在 Lean 4 + Mathlib 中积累数学形式化成果。项目在 4×H100 集群上以 Qwen3.6-27B-FP8 通过 vLLM 本地运行，前沿 API 仅作对照臂；截至 2026-09-30 的校准期内 CVFN 为 0，所有通过验证的产物均在重复 Mathlib 已有内容。