kumori-ai 开源 sparebrains：用闲置免费模型池自动解 Lean 4 竞赛数学题

kumori-ai 发布 sparebrains 仓库，把 60 多个免费档模型组成的路由池闲置算力用于 Lean 4 形式化的竞赛数学证明，由 Lean 证明内核而非人工或模型判分。题目分 primer、MIL、miniF2F 分级等 578 道，每题每条模型通道最多试三次，验证通过率达 0.5 即算通关；每晚 22:00 和 03:00（太平洋时间）跑两轮扫描，全部转录存入 Postgres 并在 sparebrains.kumori.ai 公示，验证标准为 lake env lean 退出码为 0、无 sorryAx、公理仅限 propext、Classical.choice 和 Quot.sound，仓库以 Apache-2.0 许可并给出完整复验命令。