学习与研究AI 资源
sparebrAIns：用免费闲置算力与 Lean 4 内核验证进行机器可核验数学证明的开放协作平台
kumori-ai/sparebrains · sparebrAIns: idle free-tier LLM compute pointed at machine-verified math. Lean 4 kernel is the judge.
ELI5：它是什么，解决什么问题
sparebrAIns 是一个开放协作项目，把免费层 LLM 和免费 GPU 算力指向用 Lean 4 形式化的数学问题，由 Lean 4 内核作为机器裁判判定每个提交的证明是否成立。项目维护 378 道 Lean 4 形式化题目（来自 Natural Number Game、Mathematics in Lean、miniF2F 等），通过模型跑道、中继接力、证明修复循环（修复形式、挖洞、Lean 自动化、子目标拆分）和志愿者 Agent 提交等机制求解，并把每次尝试、被拒尝试与最终通过证明一并公开记录。README 报告其修复工具能把免费模型的通过率从 44.8% 提升到 56.1%，最小模型提升最大。
核心能力与快速开始
★ 2 · Lean
- 能做什么
- 用 Lean 4 内核作为裁判，对形式化数学问题的候选证明进行机器核验（编译通过、无 sorryAx、公理审计仅限三个标准公理）；提供模型跑道、中继接力、证明修复循环与子目标拆分、公开问题线程与志愿者 Agent 接管、以及在免费 GPU 上运行开源证明器（Goedel-Prover-V2-8B）的通道；公开每次尝试的台账与已核验证明。
- 适用场景
- 想参与开放形式化数学证明的开发者或 Agent 用户可以把自己的模型配额指向公开问题；研究者可参照其跑道与修复循环做免费模型能力测量与消融对比；项目还计划把可核验成果交付给癌症研究者等外部使用方。
- 项目形态
- 资料合集
- 部署方式
- 未说明
- 主要依赖
- 运行核验需要 Lean v4.33.1 与 mathlib v4.33.1；参与方式可只提交证明由项目侧裁判核验，无需自行运行全部流程；具体硬件与 API 成本未说明。
- 使用限制
- 项目目标是不花钱，但可用的免费额度、算力配额等条件未说明；材料未说明可商用性或部署限制；只解决了部分基准题目，README 自述免费模型在自动化留下的开放步骤上 176 次引理询问中 0 次成功，需要更强证明器。
- 许可证
- Apache-2.0
- 最近推送
- 2026-10-22 06:04
资料检查：2026-10-22 07:00 · 卡片整理：2026-10-22 07:00
卡片由 AI 根据仓库资料整理，未进行安装或运行验证
讨论 0
登录后参与讨论，阅读资讯无需注册。
还没有评论，来分享第一个看法。