形式化验证

sparebrAIns：用免费闲置算力与 Lean 4 内核验证进行机器可核验数学证明的开放协作平台

kumori-ai/sparebrains · sparebrAIns: idle free-tier LLM compute pointed at machine-verified math. Lean 4 kernel is the judge.

sparebrAIns 是一个开放协作项目，把免费层 LLM 和免费 GPU 算力指向用 Lean 4 形式化的数学问题，由 Lean 4 内核作为机器裁判判定每个提交的证明是否成立。项目维护 378 道 Lean 4 形式化题目（来自 Natural Number Game、Mathematics in Lean、miniF2F 等），通过模型跑道、中继接力、证明修复循环（修复形式、挖洞、Lean 自动化、子目标拆分）和志愿者 Agent 提交等机制求解，并把每次尝试、被拒尝试与最终通过证明一并公开记录。README 报告其修复工具能把免费模型的通过率从 44.8% 提升到 56.1%，最小模型提升最大。