Skip to content

Latest commit

 

History

174 Commits

Folders and files

NameName
Last commit message
Last commit date
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Vibe Mathematics — 多代理数学问题求解与验证框架(四架构)

English | 中文

npm License: MIT GitHub stars

运行在 DeepSeek Harness 内的一组 agent preset(vibe-math-v2 / vibe-math-v3 / vibe-math-v4 / vibe-math-v5), 用多代理协作自动求解数学问题并对结论做多代理交叉验证。四个预设共享「断点续跑、 中途人工干预、进度汇报、自然语言驱动」底座能力,但采用四代不同的求解架构: 💡 四个架构同级——vibe-math-v2 与 vibe-math-v3 是经典架构(成熟可用、持续维护),vibe-math-v4 是「常驻自组织合作研究」架构、vibe-math-v5 是最新的「研究所体系」(两者均标注为实验性);根据你的实际需求自行选择(详见下方「怎么选」)。

  • vibe-math-v2(概率驱动 · JSON 数据层)· 经典:qs.json 问题清单 + Propos/ 命题库 + 概率驱动调度 + 代码启发式调度;
  • vibe-math-v3(第三代 · 论文式 md + 规划代理 + 方法库)· 经典:全部知识以 Markdown 论文/研究报告式 存储与续写(Problems/ 问题清单+依赖+来源动机、Progress/ 研究日志、Propos/ 命题库、Methods/ 通用理论发明库、Verified/ 绝对可信);调度前由规划代理自主制定接下来 N 步计划;解决过程中发明的理论/框架/工具/方法/思想由 Method Keeper 沉淀为可复用方法体系(如发明群论、泛函分析那样)。
  • vibe-math-v4(第四代 · 常驻自组织合作研究)🧪 实验性:一组持久化常驻子代理互相留言 + 开会,自主决定一切任务安排(无中央调度);各自沉淀进度/命题/方法/子问题库并互相查阅;验证**仅当全体常驻一致(真 或 假)**才写入 Verified/,否则留库附概率;上下文达阈值自动 /compact;仅当全体一致认为原问题已解决才停止。
  • vibe-math-v5(第五代 · 研究所体系)🧪 实验性 · 最新:把常驻升级为一座研究所——院士(领头人 / 组织与协调中心,负责拆解与分派、定优先级、主持会议、督导进度)+ 常驻研究员(有表决权,可自主雇佣/解雇自己的临时工)+ 临时工(无表决权);有公共规章、群聊与会议、compare-and-set 任务板、真实解雇;≥ m 票布尔一致才写入 Verified/(反向票阻塞、弃权不计票、未达门槛留库附平均概率);状态存于研究所目录下的加固 JSON State/<研究所>.v5state.json(串行写、读前必 load),不写入宿主会话日志,零 token 成本。

安装本插件包(或手动复制预设)后,DSH 的预设选择器里会出现四个 agent preset。


🧭 导航:我想要……→ 从这里开始


🧩 架构图(v2 + v3 + v4 + v5)

静态架构图;完整流程说明见 docs/架构图.md(v1 历史架构图;v2 起目录布局已变更)与 vibe-math-v5/架构图.md(v5 全套细节图); 可编辑生成脚本:中文 v2/v3 海报由 matplotlib 脚本生成 v2 / v3(matplotlib → PNG); 英文版 v2/v3 由零依赖 Node 脚本生成 v2-en / v3-en(→ SVG); v4 / v5 (零依赖 Node → SVG,node docs/generate_framework_diagram_v4.mjs,加 --lang=en 生成英文版 示例图/框架图-v4-en.svg)。 v4 起改用 SVG:纯文本、diff 友好、任意缩放不糊;需要 PNG 时用无头浏览器截图(命令见生成脚本头部)。

Vibe Math V2(概率驱动 · JSON 数据层)· 经典

Vibe Math V2 架构图

一句话流水线:qs.json 按优先级取问题 → Explorer 拆方向(全死路则重派生)→ 每方向一个 Solver 多轮迭代(引理进 Propos/、解法回 qs.json,概率均 <1)→ 调度器选 r(命题 / 命题+证明·证伪 / 问题+解法)派 ≥3 验证器独立审查→辩论→裁决 → 概率=1 自动收口(问题 solved、命题 1/0,优先级置 never);全程状态落盘,resume 断点续跑,reportMode 可 file/push/both 汇报。

Vibe Math V3(论文式 md + 规划代理 + 方法库)· 经典

Vibe Math V3 架构图

一句话流水线:全部知识以 Markdown 论文/研究报告式存储与续写(Problems/ 问题清单含依赖/后生问题来源动机、Progress/ 研究日志按方向按轮续写、Propos/ 命题库、Methods/ 通用理论发明库、Verified/ 绝对可信)→ 调度前调度器构造状态简报并调用规划代理,规划代理一次性安排接下来 N 步(spawn solver/verifier/explorer/method-keeper、interrupt、promote、wait),代码校验后执行(超出并发的动作排队跨 tick 消费;规划失败自动回退 v2 式启发式)→ 验证器独立审查→辩论→近共识裁决(同侧且均值 ≥0.85/≤0.15 取均值,修复 v2 flat 误判)→ 概率=1 收口并生成 Verified/ 卡 → 求解器的 methods_used/new_inventions 上报由 Method Keeper 沉淀/完善方法库(可组成体系层级、跨项目复用)。

Vibe Math V4(常驻自组织合作研究)🧪 实验性

Vibe Math V4 架构图

上面这张 SVG 由零依赖脚本生成:node docs/generate_framework_diagram_v4.mjs(纯 Node、无 Python/matplotlib 依赖; 生成时会估算文字宽度,任何一行溢出容器都会告警并以退出码 1 结束)。

一句话流水线:起始产生 N 个常驻子代理(continuable,持久上下文)先各自头脑风暴、产出初始见解/方向 → 此后所有任务安排由它们互相留言 + 集体开会自主决定(框架只做消息总线/会议/任务板/产物沉淀,绝不分配任务);每个常驻把有价值的产物按价值程度 / 动机用途计划 / 自身概率估计沉淀到自己的 Progress/<id>/、Propos/<id>/、Methods/<id>/、Subproblems/<id>/ 库,并可互相阅读;验证由它们自行商议发起,**仅当全体常驻一致(真或假)**才写入 Verified/,否则留库附概率;常驻上下文量达阈值(默认 66%)自动 /compact;仅当全体一致认为原问题已解决才停止;可随时人工干预/增开/关闭常驻,支持断点续跑。

说明:V4 去掉 v3 的中央规划器与确定性角色(explorer/solver/verifier/planner/method-keeper),把"研究者"本身作为主体。详见 vibe-math-v4/实现方案.md。 保活机制(分级保活 A+B + 死锁看门狗):团伙空闲超 activityTimeoutMs 会收到自驱动 CHECKPOINT(建议继续解决/发消息/提议任务,而非"是否要停止"),且并行填充——A 分支一次尽量填满 maxParallel 并发预算(同一时刻唤醒多个空闲常驻,而非"只唤醒 r1、结束后再 r2"的串行),邮箱投递也并行送达多个空闲收件人;唤醒失败会自动重新武装心跳;若团队空闲且无新产物超过 stallAutoMeetingMs(默认 6 分钟),框架会自动召集一次同步会议让常驻们自行决定下一步;若某次会议/验证卡死(超过 2×activityTimeoutMs 仍无新的发言/投票),框架会自动放弃该会议/验证并回到正常自组织,避免一个坏掉的会议永久卡住整个团队;会议不抢占验证——验证进行时会议请求会暂存,验证做完再补开(保持一致共识的"求真"环节不被协调讨论打断)——框架始终只促成、从不指派任务。


Vibe Math V5(研究所体系)🧪 实验性 · 最新

一句话定位:把 v4 的"一群互相留言的常驻"升级为一座研究所——有院士(领头人)、常驻研究员、 临时工三类职员,有所内公共规章,有群聊与会议,有自主雇佣/解雇,并且 任何结论都必须由至少 m 名有表决权者一致给出布尔概率 1 或 0 才能写入 Verified/。

Vibe Math V5 架构图

图源与全部细节图(成员生命周期、一轮时序、共识状态机、会议流程、调度优先级、状态折叠、 提示词构成、任务板、职权矩阵):vibe-math-v5/架构图.md。 上面这张 SVG 由零依赖脚本生成:node docs/generate_framework_diagram_v5.mjs。

flowchart TB
    OFF["👤 所办(会话根代理 / 人)<br/>不研究 · 不投票 · 只汇报与转达指令"]
    subgraph INST["🏛️ 研究所(所内自治:编制、组织与分派都在成员之间完成)"]
        ACAD["院士 acad —— 领头人 / 组织与协调中心<br/>L1 全所视图 · L2 分派 · L3 优先级<br/>L4 主持会议 · L5 督导 · L6 调人 · L7 对外"]
        RES["常驻研究员 r-n<br/>有表决权 · 可自主雇佣/解雇自己的临时工"]
        TMP["临时工 t-n<br/>无表决权 · 为特定任务临时雇入"]
    end
    subgraph FW["⚙️ 框架 vibe-v5 —— 只是媒介(middleware),绝不指派任务"]
        M["消息中继 · 会议/辩论 · 任务板 CAS+DAG<br/>m 票共识验证 · 上下文与活性 · 编制与雇佣 · 调度器"]
    end
    PROJ["💾 State/&lt;研究所&gt;.v5state.json(加固 JSON 权威源)<br/>12 类事件 · 纯折叠 applyV5Event · 串行写 · 恢复=读前必 load"]
    FS["📁 Members/&lt;id&gt;/* · Shared/* · Verified/ · Problems/"]
    RULE{{"求真门槛:布尔一致 且 布尔票 ≥ m = min(quorumCap, 在册有表决权人数)"}}
    OFF <-->|"vibe_v5_* / /v5 命令 ↔ status / report"| M
    M <-->|"每轮提示词 ↔ 单个 JSON 回执"| ACAD
    M <-->|"每轮提示词 ↔ 单个 JSON 回执"| RES
    M <-->|"每轮提示词 ↔ 单个 JSON 回执"| TMP
    ACAD -.->|"分派 / 督办 / 主持会议(所内组织,非框架行为)"| RES
    ACAD -.-> TMP
    M <--> PROJ
    M <--> FS
    M --> RULE
Loading

一句话流水线:所办(会话根/人)configure → start 建所 → 院士(academician,组织与协调中心)拆解原问题并分派任务、定优先级、主持会议、督导进度;常驻研究员各自研究并持有表决权,临时工可按需雇入(无表决权、可被真实解雇)。框架只做媒介,绝不指派任务;一切结论都要 ≥ m = min(quorumCap, 在册有表决权人数) 张布尔票且全部同向才写入 Verified/(反向票阻塞、弃权不计票但计入平均概率,未达门槛留库附平均概率);会议与验证双向互斥;状态写在研究所目录下的加固 JSON State/<研究所>.v5state.json(零 token 成本、串行写、读前必 load);仅当全体有表决权者都认为原问题已解决才结题。

职位与职权、求真规则细节、运行机制、状态与持久化、提示词构成、研究所目录、工具面、与 v4 的差异:见 vibe-math-v5/架构图.md §13「从 README 移入的 v5 说明」(原文保留);参数见参数速查表,最终论文见 docs/final-paper.md。


✨ 功能特色

  • 最终论文(四个预设默认开启):收口时自动撰写一篇只整理已有证据的完整论文,且论文阶段发生在 run 被标记完成之前;产物在 Paper/<id>/{paper.md,paper.tex,paper.pdf,paper.meta.json,paper.log.md}。参数 finalPaper(默认 true)/paperFormat(默认 both)/paperLanguage(默认 zh)/paperCompilePdf(默认 true)(v4/v5 另有 paperEditor),手动 /vN paper [lang=] [format=] [editor=] [force];PDF 需要宿主上有 LaTeX 引擎(中文优先 xelatex),否则仍交付 tex+md。完整契约与用法见 docs/final-paper.md。
  • 多代理自动求解:主代理把问题交给调度器,调度器派发 explorer / solver / verifier(v2/v3)与 planner(规划代理,v3)、method-keeper(方法整理代理,v3) 等子代理协同求解,你无需逐节点手操。
  • 多代理交叉验证:每个结论交给 ≥3 个「严苛审稿人」独立审查 → 辩论(交流群)→ 裁决(v3 默认近共识裁决:同侧且均值 ≥0.85/≤0.15 取均值,避免"0.9 vs 1"被误判成 0.5)。
  • 论文式 Markdown 知识库(v3):问题清单(含问题间依赖、后生问题产生原因与计划)、研究日志、命题、方法库全部以 md 论文/研究报告式书写与续写(方向重派生时旧方向的日志自动归档保留);只有 Verified/ 与验证器判真/假的对象绝对可信,其余 md(含方法库未验证断言)仅作经验参考。
  • 通用理论发明库(v3):解决过程中发明的理论体系/框架/工具/方法/思想(含经验性总结)经 methods_used/new_inventions 上报,由 Method Keeper 沉淀为 Methods/ 方法卡(可组成体系层级、跨项目复用),像"解决方程时发明群论"一样形成系统化方法理论体系。
  • 规划代理调度(v3):调度前调用规划代理,根据实际情况(问题依赖/存活率/可验证对象/并发预算/上次计划结果)自主选择最优调度方案,一次安排接下来 N 步各代理任务;规划失败自动回退启发式。
  • 知识沉淀:验证通过的结论晋升进 Verified/ 可信知识库(v2/v3 另有 Propos/ 命题库),供后续方向复用。
  • 断点续跑:调度状态、任务栈、代理注册表、决策队列、验证器历史准确率等全部落盘;重启后 resume 即可恢复(v2/v3 用进程纪元区分"同进程暂停→恢复"与"跨进程重启";v3 的 md 本身即叙事断点)。
  • 中途人工干预(并继续):auto / manual 模式随时切换;manual 在关键节点挂起决策等你 approve/reject/override(v3 新增计划审批门与方法晋升门);可对任意子代理发消息 / 中断。
  • 按项目隔离:每个数学问题一个独立项目文件夹,互不干扰,可随时切换。
  • 多会话并行隔离:DSH 的 agent preset 是 standing mount(同一 preset 的所有会话共享一个插件实例),插件内部按根会话 id 隔离全部运行状态——两个会话可以同时各跑一个项目,各自的子代理会正确挂在自己会话名下,调度器 / 参数 / 决策队列 / 当前项目互不干扰(v3 另有项目锁,同一项目同一时刻只被一个会话调度)。当前项目按会话分别持久化(VibeMath/current.<会话id>.json)。
  • 子代理权限可调控:可限制子代理允许/禁止的工具、每轮外部工具调用上限,并明确告知其可读 Verified/、Propos/、Methods/、Reliable/ 与进度日志。
  • 可配置:vibe_math_setting.json(含注释)自定义默认参数;/vibe setup 交互式问答配置。
  • 自然语言控制:主代理充当「助手 + 汇报者」,你把需求说成人话,它自己调用工具、汇报进度、配置参数。

v4 / v5 特有:

  • 常驻自组织(v4):起始产生 N 个持久化常驻子代理,此后所有任务安排由它们互相留言 + 开会自行决定(框架只做消息总线/会议/任务板,绝不分配任务)。
  • 研究所体系(v5):在 v4 的自组织之上引入现实研究所的组织形式——院士(领头人)负责拆解、分派、定优先级、主持会议、督导进度;常驻研究员有表决权并可自主雇佣/解雇自己的临时工;临时工无表决权;全部组织动作都由所内成员完成,框架仍然只做媒介。详见上方 Vibe Math V5 一节。
  • 可调的一致性门槛(v5):对象要进 Verified/,需要 ≥ m = min(quorumCap, 在册有表决权人数) 名有表决权者投出一致的布尔票(全 1 或全 0);反向票阻塞、弃权不计票但计入平均概率;未达门槛则留库附平均概率与完整辩论录,不强行裁决。
  • 零 token 成本的状态持久化(v5):研究所状态写在研究所目录下的加固 JSON 里(State/<研究所>.v5state.json),不进模型上下文;跨进程与同进程恢复走同一条代码路径(读前必 load)。
  • 真实可逆的编制(v5):雇佣会创建常驻子会话,解雇会取消在途回合、释放子会话、收回其任务并丢弃未投递邮件;代号永不复用。
  • 人可读镜像(v4/v5):编制表、任务板、会议纪要、辩论录、结题记录都以 Markdown 落盘,人随时可读;但权威状态不在这些文件里(v5 在 State/<研究所>.v5state.json),所以手工改坏它们不会破坏研究所。

🧮 Lean 形式化验证(四个架构共用,可调开关)

它改变的不是"更严格一点",而是审查对象本身。 m 个代理一致认为"这是对的"仍然是共识—— 排除不了共同误解;Lean 通过是机器核对。于是剩下的唯一不确定项缩小为一个人能有效审查的问题: Lean 代码里的定义 / 对象 / 条件 / 假设 / 结论,是否与命题原文完全一致(忠实性)?

  • 开关 formalVerify(四个架构同名,默认 'off'):'off' 是真正的无操作(提示词里不出现任何 Lean 内容、不写入任何形式化状态、验证流程与门禁完全不变;五个工具仍注册可用,persona 始终列出它们,否则这个开关不可发现、也无从打开);'encourage' 鼓励但不强制(验证时按实现难度自行决定是否形式化,一旦 Lean 通过,审查重心转为忠实性,不设门禁);'require' 强制——真/假结论必须满足「Lean 已通过」或「显式记录了阻塞原因」,否则本次裁定不生效(记为未定论、原因 formal-required、写入「形式化待办」)。相关参数:leanCommand(默认 lean)、leanArgs(配合 lake env lean)、leanTimeoutMs(默认 120s)。

  • ⚠️ 忠实性缺陷 ≠ 命题为假(重要):Lean 通过只保证"这段代码过了内核",不保证它说的就是命题想说的。表决者逐条核对后发现 Lean 代码与命题原文不一致(写窄 / 写宽 / 换了对象 / 漏了条件)时:不得投 0(投 0 的含义是"该命题为假"——那会把"形式化不合格"记成"命题被证伪",v5 的全 0 一致规则下甚至写进 Verified/ 标注假,用来求真的机制反而伪造出一个错误的否定结论);正确做法是投一个严格介于 0 与 1 之间的值(记为弃权)+ 用回执 formal:{decision:'defect', note:'<具体偏差>'} 记录偏差,框架随即撤回这条证明的「已通过」状态(降级为 attempted、删除 Verified/Lean/<id>.lean、宿主删不掉时改写为"已撤回"说明、写入「形式化待办」),require 档下本次裁定不定论(encourage 档没有门禁,不得声称框架会强制搁置);只有表决者独立于这份 Lean 代码也能确定命题为假(并能给出独立理由)时才投 0。

  • 回执通道与三条硬要求(不调用 Lean 工具的成员也能留下判断,require 档下必须留):回执字段 "formal": {"target":"<对象id>", "decision":"used|blocked|defect", "file":"Formal/<对象id>.lean", "note":"难度判断/阻塞原因/具体偏差"};decision='blocked'/'defect' 时 note 必填(缺则整条拒绝),used 只把对象记为 attempted,off 档下该通道失效(否则 off 就不是真正的无操作)。另外三条:注入文本里的工具名一律全称(<prefix>_lean_archive 不是 lean_archive——缩写不是注册名);归档可复用定义/引理前先跑通,跑不通不许进库;工具链缺失(LEAN_NOT_FOUND 解析不到可执行文件 / NO_SUBPROCESS 宿主没有 subprocess 服务)时把代码写下来归档并在 note 写明"宿主无 Lean 工具链"——这算显式阻塞原因,门禁据此放行,不会因为装不了 Lean 而卡死。

  • 归档位置:<VibeMath 根>/Formal/Lib|Proved/(跨项目可复用定义与已证引理,各带 Index.md 索引,写新定义前先查这里);项目内 Formal/<对象id>.lean 是对象的工作文件(旁边有 Index.md 与 require 档的 TODO.md),Verified/Lean/<对象id>.lean 是归档证明(v5 在 Projects/<项目>/Institutes/<所>/ 下)。

  • 五个工具(每个架构一套,前缀跟随各自命名):<prefix>_lean_run 在宿主 subprocess 服务上执行 Lean(leanAsync=true 时入队即返回 {async:{jobId,state}},否则同步返回 {ok, exitCode, ms, stdout, stderr}),绝不抛异常(缺工具链 → LEAN_NOT_FOUND、超时 → LEAN_TIMEOUT、越界路径 → 拒绝);<prefix>_lean_archive:kind='def'/'lemma' 归档到跨项目 Formal/Lib|Proved(同内容去重),kind='proof' 写 Formal/<target>.lean 并只在作业 settled(ok) 时写 Verified/Lean/<target>.lean 标记该对象为 Lean 通过,kind='blocked' 记录显式难度判断/阻塞原因(原因必填);<prefix>_lean_lib 重建并返回三处索引、逐对象状态与后台作业,写新定义前先查重复用;<prefix>_lean_read 取回归档原文(逐字复用,限 Formal/Lib|Proved、64KB);<prefix>_lean_job 查看/等待后台编译作业(只读)。例如 v5 是 vibe_v5_lean_*,v2/v3 是 vibe_math_lean_*,v4 是 vibe_v4_lean_*(各有 run / archive / lib / read / job 五个)。

  • 边界(有意为之):框架不内置 Lean(不装工具链、不下载依赖;工具链缺失时优雅降级并如实记录);框架不判断忠实性(那是代理/人审查并投票的对象,框架只负责把审查焦点换成忠实性);Lean 通过 ≠ 命题为真——它只表示"这段形式化代码通过了内核检查"。

完整契约(参数、路径、状态迁移、提示词语义、门禁位置、索引格式、测试要求)见 docs/formal-verification.md。四个预设的 persona(主代理收到的提示词)都完整列出了这五个工具与八个参数,并且 prefix 与 text 两个块逐行一致(只允许第 0 行不同);这一层由 audit-persona-surface.test.mjs 与 audit-persona-sensitivity.mjs 守护——加入本特性时正是在四个预设里发现了"工具已注册、persona 从未列出"的缺陷(详见随包发布说明)。


🚀 安装

两种安装方式,任选其一(也可并存):

方式 A:作为插件包一键安装(推荐,同时装出四个预设)

桌面版在「设置 → 插件」里安装 dsh-vibe-math;命令行 profile 用:

dsh plugin --profile <你的 profile> add dsh-vibe-math
# 或从 GitHub 直装:
dsh plugin --profile <你的 profile> add github:ChongCyrus/Vibe-Mathematics

之后新建会话,预设选择器里选择 Vibe Math V2(v2,经典)、Vibe Math V3(v3,经典)、Vibe Math V4(v4,常驻自组织)或 Vibe Math V5(v5,研究所体系)即可——四个架构同级,按实际需求自选(见「怎么选」)。 两个 DSH 世代的落点不同,本包自动适配:

  • DSH ≥ 0.1.7(当前):agent preset 由组合行声明。本包在 cordis.patch.yml 里声明四个 preset(每行把该 preset 的完整插件清单交给宿主的 agentPresets 服务注册),不往 ~/.dsh/.agent-presets/ 写任何东西——该目录自 0.1.7 起不再被读取。
  • DSH ≤ 0.1.6:preset 仍是目录形式,安装器把四个 preset 写入 ~/.dsh/.agent-presets/(vibe-math-v2/ … vibe-math-v5/);同一份 cordis.patch.yml 里的声明行在这些版本上什么都不注册,因此旧版启动不会报错。

升级包版本后重启 DSH,受管内容会被整体替换成新版本的字节——包括你手动改过的文件。 这是有意的:一个"一半旧版、一半新版"的 preset 会挂不上或行为诡异,而你在外面看不出来。被替换掉的手改内容不会丢:目录形式下原文会先备份到 ~/.dsh/.agent-presets/.vibe-math-backup/<旧版本>/<preset>/,文件名会在日志里列出。 要自定义 preset 就别改受管内容——复制一份(预设选择器里的复制动作,或在自己的 bundle 里用新的 id 声明)。注意:在当前 DSH 里你若为同名 id 保存了自己的声明,本包会放弃注册并打印一行说明,以你的声明为准。

方式 B:手动声明(自定义 / 二次开发)

  • DSH ≥ 0.1.7:把 vibe-math-vN/agent.cordis.yml 整段作为 plugins 放进一个声明行——既可以照抄本包 cordis.patch.yml 里的 dsh-vibe-math/preset-declaration 行,也可以用宿主自带的 @deepseek-ai/dsh-agent-preset 行;把这个 bundle 装进你的 profile 即可。完整规则见 DSH 自带技能 editing-cordis-compositions。
  • DSH ≤ 0.1.6:把 vibe-math-vN/ 下的 agent.cordis.yml / preset.yml / vibe-math-vN.js 复制到 ~/.dsh/.agent-presets/vibe-math-vN/。

新建会话后在 preset 选择器里选 「Vibe Math V2」 / 「Vibe Math V3」 / 「Vibe Math V4」 / 「Vibe Math V5」;会话启动后即可使用:v2/v3 的工具是 vibe_math_*、v4 是 vibe_v4_*、v5 是 vibe_v5_*;输入框键入 /vibe、/v4、/v5 有自动补全。

改过 preset 定义后需重启 DSH 进程再开新会话(preset 的 standing mount 会缓存到进程退出)。

DSH 版本适配与依赖

  • 形态依赖(两条线,本包一份 bundle 全兼容):bundle patch 机制(cordis.patch.yml,dsh.bundle.patch 必须是字符串——0.1.5/0.1.6 会把该值直接送进 path.join,数组会让 profile 起不来);DSH ≥ 0.1.7 走 组合行声明(agentPresets 服务),DSH ≤ 0.1.6 走 ~/.dsh/.agent-presets/<id>/ 目录 + preset picker。
  • 宿主插件行:agent.cordis.yml 引用宿主提供的 @deepseek-ai/dsh-* 插件行(persona、agent-instructions、tool-bash/pwsh、tool-fs/fs-search、tool-jobs、skill-filesystem、tool-skill、tool-goal、plan-mode、compaction、subagent/workflow、ask-user、todo、web 等,约 21 个唯一包名)。宿主缺行会导致 preset 挂载失败(会话启动时报错)。
  • 宿主服务 API:预设插件消费 subagents(startContinuable / sendMessage(续做/唤醒;followup 仅为 Agent 对象方法、不是 subagents 服务方法)/ interrupt / drainContinuableChildren(v5 用于真实解雇))、agents(get/roots)、tools(register/restrict)、commands(register)、fs(resolve/stat/readText/writeText/listDir),以及可选 subprocess / sandboxPolicy / compaction。这些 API 形状随 DSH 版本演进;本项目已在 dsh-v0.2.0-rc.2 上逐项核对并适配(package.json 的 dsh.testedVersion),并同时对齐 0.1.5-rc.2。注意:DSH 0.1.2 起 subagents.startContinuable 的 agentOptions / toolFilter 需要宿主 provider 声明对应 capability(spawn / fork 进程内 provider 均支持,v4/v5 指定成员模型/路由与工具权限依赖于此)。
    • v5 的研究所状态只写在 State/<研究所>.v5state.json(加固 JSON、串行写、读前必 load)。v5 不再把研究所事件写进宿主会话日志:DSH 的会话持久化遇到日志里不认识的事件类型会拒绝加载整个会话(除非写入方标记 ignorable: true,而 Session.append 无法设置该字段),那会让你自己的会话在下次恢复时打不开。
    • 常驻数量有宿主上限:DSH ≥ 0.1.7 对每个根代理的存活 continuable 子代理设了上限(subagent 行的 maxActiveSubagents,默认 8)。v4/v5 会在撞到上限时给出明确提示、把该次派生推迟到下一轮,而不是让启动循环崩在半途。

    2026 兼容性修复要点(详见 docs/COMPAT-AUDIT-ROUND2.md):① tools.restrict() 对未注册的工具名抛错,而 filter 在建立子代理时应用,故权限名表必须只含本部署真正注册的名字——v2/v3 原先硬编码 web/fetch/bash(其中 bash 在 Windows 被 disabled)会导致"想收紧权限时子代理永远起不来";② v4 的真实 /compact 原先在 subagent/end 里查 agents.get(),但该事件在子代理已被移出注册表之后才触发,属死代码,已改为在 subagent/start 捕获引用;③ 可选服务改为惰性读取,不再在 apply() 快照(否则挂载顺序会让 subprocess 永久为 undefined 而静默不建目录)。

  • DSH STORE 兼容声明:package.json 的 dsh.compatibility.dshReleases 对每个完整 DSH 版本逐项声明 compatible / incompatible / unknown(当前声明 0.1.2-alpha.4 … 0.2.0-rc.2 共 11 个版本为 compatible,实测目标为 0.2.0-rc.2);engines.dsh 为 >=0.1.2-alpha.4 <0.1.3-0 || >=0.1.3-alpha.2 <0.1.5-0 || >=0.1.5-alpha.1 <0.1.6-0 || >=0.1.6-alpha.1 <0.1.7-0 || >=0.1.7-alpha.1 <0.2.0-0 || >=0.2.0-alpha.1 <0.3.0-0;engines.node 为 ^22.19.0 || >=24.0.0。 另外声明了 peerDependencies(@deepseek-ai/dsh-base,并标为 optional):DSH ≥ 0.1.7 会用宿主自己的版本去比对插件声明的 peer 范围,不满足时跳过整个 bundle 并给出明确提示,而不是挂上一个跑不通的预设。
  • 运行时自检(版本 + 形态 + 能力):安装器(bundle 插件)每次启动时:① 按优先级探测 DSH 版本——DSH_VERSION 环境变量 → pluginManager 服务的 bundle 列表(@deepseek-ai/dsh-base 的版本即宿主版本,0.1.7+)→ @deepseek-ai/dsh-app-boot 导出的 getDshRuntimeVersion()(0.2.0+ 的公开 API)→ @deepseek-ai/dsh/package.json(全局 0.1.x 安装),日志会写明来源;探测到且未被 dshReleases 声明为 compatible 时给出明确提示。② 判断 preset 形态:从 loader 入口树里是否挂了 @deepseek-ai/dsh-agent-preset(或其 registry)判断本宿主是"组合行"还是"目录",据此决定是否同步 ~/.dsh/.agent-presets/——新宿主上会跳过并在日志里说明旧目录可安全删除。③ 能力自检(真正的挂载门槛):subagents/agents/tools/commands/fs 为必需(缺失即 warning),subprocess/sandboxPolicy/compaction 为可选(缺失只提示"功能会静默降级"),另含 fs.resolve 返回形状检测与 subagent agentOptions/toolFilter capability 检测。preset 挂载失败时先看 DSH 日志里的自检 warning。
  • 升级路径:DSH 升级后无需重装本包;升级本包用 dsh plugin --profile <你的 profile> add dsh-vibe-math@latest(dsh plugin 的 --profile 是必填项;用 add 而不是 update,因为 profile 里可能把版本钉成精确值,那时 update 不会跨过去),重启 DSH 后(DSH ≤ 0.1.6 的目录形式下)安装器会把四个 preset 的受管文件整体更新到新版本(改过的文件同样被替换,原文先进 <presetRoot>/.vibe-math-backup/;DSH ≥ 0.1.7 的 preset 来自组合行,安装器不写任何文件)——见上文「安装」说明。

🧭 四个预设怎么选

💡 四个架构同级,按你的实际需求自行选择:

  • 选 vibe-math-v2(概率驱动 · JSON 数据层),如果你:
    • 偏好结构化 JSON 数据(qs.json / Propos/<分类>_Propos.json / Verified/ 卡),方便程序化检索与二次加工;
    • 想要成熟稳定的代码启发式调度(优先级 + 概率,行为可预期、不依赖规划代理的"临场发挥");
    • 不需要方法库沉淀 / 论文式叙述,数据以字段为主即可。
  • 选 vibe-math-v3(论文式 md + 规划代理 + 方法库),如果你:
    • 偏好论文/研究报告式的自然语言知识库(问题清单含依赖与后生问题来源动机、研究日志按方向按轮续写,人类可读、可自由续写);
    • 希望调度由规划代理根据实际情况自主制定 N 步计划(更灵活,失败自动回退启发式);
    • 希望通用理论发明库——求解中发明的理论/框架/工具/方法/思想经 Method Keeper 沉淀为可复用、可体系化、跨项目扩充的方法论(像"解决方程时发明群论");
    • 接受"只有 Verified/ 绝对可信,其余 md 为经验参考"的可信分层。

两者都成熟可用、持续维护,且都支持断点续跑、人工/自动干预、进度汇报、多会话隔离、命题晋升、近共识/加权裁决等核心能力;切换成本低(同一套 vibe_math_* 工具与 /vibe 命令、同一套参数体系)。

  • 选 vibe-math-v4(常驻自组织),如果你想要一组持久化常驻子代理互相留言开会、完全自组织(无领头人、无中央调度),并且能接受"全体一致才定论"这种严格门槛。
  • 选 vibe-math-v5(研究所体系),如果你想要:
    • 有组织的自组织——现实研究所那样有领头人(院士)负责拆解、分派、定优先级、主持会议、督导进度,但判断仍归每个人自己;
    • 可增减的编制——常驻研究员 + 可自主雇佣/解雇的临时工(临时工无表决权,适合处理核对、试算、资料整理等杂活);
    • 可调的一致性门槛——m = min(quorumCap, 有表决权人数) 票布尔一致即定论(因为反向票阻塞,实际门槛仍是"全部布尔票同向";只有投出布尔票的人少于 m 时才不同);
    • 零 token 成本的状态持久化——研究所状态写在研究所目录下的加固 JSON 里,不占成员上下文预算。

⚠️ vibe-math-v2 与 vibe-math-v3 是经典架构;vibe-math-v4、vibe-math-v5 是实验性架构, 四者同级、均可选择;老 vibe-math-v1 已被移除(本包仅含 v2/v3/v4/v5)。

v2(概率驱动 · 经典) v3(论文式 md · 经典) v4(常驻自组织 · 实验) v5(研究所体系 · 实验)
定位 经典(JSON 数据层) 经典(第三代) 实验性(第四代) 实验性(第五代)
核心思想 概率驱动:qs.json 问题 + Propos/ 命题库,按「正确概率 / 价值」调度 论文式 md 知识库 + 规划代理调度 + 通用理论发明库 持久化常驻子代理自组织:互相留言 + 开会决定一切任务,无中央调度 研究所:院士做组织与分派,成员各自研究;≥ m 票布尔一致才定论;临时工可按需雇入
数据 qs/qs.json + Propos/<分类>_Propos.json + Reliable/ Problems/ + Progress/ + Propos/ + Methods/(全部 md,软规范锚点 + 自由叙述)+ Verified/ Problems/ + 按常驻 id 归属的 `Progress Propos
角色 explorer → 逐方向 solver → verifier planner(规划代理) → explorer → 逐方向 solver → verifier → method-keeper(方法整理代理) N 个常驻研究者(continuable),无固定角色 院士 acad(领头人)+ 常驻研究员 r-n(有表决权)+ 临时工 t-n(无表决权,可雇可解雇)+ 所办(不研究不投票)
调度方式 代码启发式(优先级 + 概率) 规划代理产出 N 步计划(校验后执行,失败回退启发式) 无中央调度:任务由常驻互相留言/开会(框架只做媒介,不指派) 框架仍不指派;由院士拆解/分派/定优先级/督导,成员可据理反对;框架只做中继、任务板、会议与计数
收口规则 解法/证明达概率 1 即收口,never 永不调度 同 v2(近共识裁决修复 flat 误判) **仅当全体常驻一致(真 或 假)**才写入 Verified/,否则留库附概率 布尔票 ≥ m = min(quorumCap, 有表决权人数) 且全为 1 或全为 0 才写入 Verified/;反向票阻塞;弃权不计票但计入平均;(可切回 v4 口径)
停止 全解或卡死 全解/无候选 仅当全体常驻一致认为原问题已解决才停止 同 v4:全体有表决权者一致认为原问题已解决才结题
上下文 无 无 常驻上下文达阈值自动 /compact(可调) 同 v4(阈值/轮数可调,压缩后规章仍在 persona 里生效)
特设能力 命题「价值/关键性」自动晋升问题清单;reportMode file/push/both;priorityAdjust 方法库沉淀循环(methods_used/new_inventions → Method Keeper);计划审批门/方法晋升门;项目锁;后生问题「来源与动机」一等公民 常驻各自沉淀 + 互相阅读;全体一致验证;随时增开/关闭常驻、留言干预;断点续跑 v4 的全部能力,另加:真实雇佣/解雇(释放子会话、收回任务);compare-and-set 任务板 + 依赖 DAG;会议与验证严格互斥;编制镜像与结题记录;状态零 token 成本

四者都支持:断点续跑(vibe_math_resume / vibe_v4_resume / vibe_v5_resume)、人工干预与暂停恢复、 按项目隔离、子代理权限调控、自然语言驱动。四个架构同级——偏好结构化 JSON 数据与确定性调度选 v2, 偏好论文式 md、规划代理与理论发明库选 v3;v4 是完全自组织的常驻合作研究,v5 是"有领头人 + 可增减编制 + 可调门槛"的研究所体系。


🧠 架构与分工(四套并列)

V2(概率驱动 · 经典)

框架 = 主代理 + 代码调度器 + explorer / solver / verifier 三类子代理。调度器是唯一主控与唯一文件写者(子代理只返回结构化 JSON,从不写文件),按「正确概率 + 价值/关键性 + 优先级」由代码启发式决定下一步;每个验证对象交给 ≥3 个独立「严苛审稿人」审查 → 辩论 → 裁决(解法/证明达概率 1 即收口,never 永不调度)。选它:偏好结构化 JSON(qs.json / Propos/)与可预期、不依赖规划代理的确定性调度。

一句话分工:主代理负责"和人对话",调度器负责"执行与守界",子代理负责"动脑"。

V3(论文式 md + 规划代理 + 方法库)· 经典

框架 = 主代理 + 代码调度器 + 规划代理 + explorer / solver / verifier / method-keeper 四类子代理。每次准备派发时,规划代理读取状态简报(问题依赖、存活率、可验证对象、并发预算、上次计划结果)自主制定接下来 N 步计划,由调度器校验后执行(失败自动回退启发式);求解中发明的理论/框架/工具/方法/思想经 methods_used/new_inventions 上报,由 Method Keeper 提炼新方法卡并沉淀进 Methods/ 通用理论发明库。选它:偏好论文式 md 知识库、希望调度更灵活、并想要可体系化、跨项目复用的方法库。

一句话分工:主代理负责"和人对话",规划代理负责"定计划",调度器负责"执行与守界",子代理负责"动脑",Method Keeper 负责"把发明沉淀成理论"。

V4(常驻自组织 · 实验)

主体是 N 个持久化常驻子代理(continuable):没有中央调度,也没有领头人——任务安排靠它们互相留言 + 开会自行涌现(框架只做消息总线/会议/任务板,绝不指派);各自沉淀并按常驻 id 归属自己的 Progress/Propos/Methods/Subproblems 库,可互相阅读;验证**仅当全体常驻一致(真 或 假)**才写入 Verified/,否则留库附概率;上下文达阈值自动 /compact;仅当全体一致认为原问题已解决才停止(vibe_v4_resume 可断点续跑)。选它:想要完全自组织、能接受"全体一致才定论"的严格门槛。

V5(研究所体系 · 实验 · 最新)

把 v4 的常驻升级为一座研究所:院士(领头人 / 组织与协调中心:拆解、分派、定优先级、主持会议、督导进度)+ 常驻研究员(有表决权,可自主雇佣/解雇自己的临时工)+ 临时工(无表决权);框架仍然只做中继、任务板、会议与计数,绝不指派任务。定论门槛为 ≥ m = min(quorumCap, 在册有表决权人数) 票布尔一致(反向票阻塞、弃权不计票但计入平均概率、未达门槛留库附平均概率);状态写在 State/<研究所>.v5state.json(零 token 成本);会议与验证严格互斥。选它:想要"有组织的自组织"、可增减的编制与可调门槛。

v5 的完整架构(成员生命周期、一轮时序、共识状态机、会议流程、调度优先级、状态折叠、提示词构成、任务板、职权矩阵)见 vibe-math-v5/架构图.md;文字规格见 vibe-math-v5/实现方案.md。


📁 目录结构

只列顶层与高价值路径;每个文件的完整语义见各预设的 实现方案.md(v2 · v3 · v4 · v5)与 vibe-math-v5/架构图.md。

v2(概率驱动 · 经典)

<VibeMath>/Projects/<项目>/
├─ qs/qs.json                   # 问题清单(概述/已解决/解法+正确概率/优先级)
├─ Propos/<分类>_Propos.json     # 命题库(布尔估计/证明·证伪/价值·关键性)
├─ Verified/                    # 定论事实索引
├─ Reliable/                    # 可信参考文献(只读,用户放入)
└─ VibeMath_State/              # 调度器私有持久状态(断点恢复用)

v3(论文式 md + 规划代理 + 方法库)· 经典

<VibeMath>/
├─ Methods/                     # 【全局】跨项目通用理论发明库(晋升自项目级)
├─ Formal/{Lib,Proved}/         # 跨项目可复用定义 / 已证引理(Lean)
└─ Projects/<项目>/
   ├─ Problems/ Progress/ Propos/ Methods/     # 论文式 md 知识库(软规范锚点 + 自由叙述)
   ├─ Verified/{命题,问题}/                      # 绝对可信(只读)
   ├─ Logs/{Verification,Plans}/  Logs/报告.md   # 辩论录 / 调度计划 / 论文式进度报告
   └─ State/                                     # 索引、项目锁、进程纪元

v4 / v5(常驻自组织 / 研究所体系 · 实验)

<VibeMath>/Projects/<项目>/
├─ Progress|Propos|Methods|Subproblems/<常驻id>/   # v4:按常驻 id 归属
└─ Institutes/<研究所>/                             # v5
   ├─ Members/<代号>/{Progress,Propos,Methods,Subproblems}/
   ├─ Shared/{Chat,Meetings,Debates}/  Shared/TaskBoard.md  Institutes.md
   ├─ Verified/<类型>/<id>.md                      # 定论(只读)
   └─ State/<研究所>.v5state.json                  # ★ 权威状态(加固 JSON、串行写、读前必 load)

铁律(四套):v2/v3 的调度器是唯一文件写者(v3 另支持代理直接写 md,靠 vibe_math_claim_write/vibe_math_release_write 写锁保证同一文件同一时刻只有一个写者);只有 Verified/ 与标注"已验证·真/假"的卡片绝对可信,其余 md(含 Methods/ 里未验证的断言)只是经验参考;v5 的权威状态只写在 State/<研究所>.v5state.json,上面其余文件都只是镜像/工作区(手工改坏不会破坏研究所),成员只写自己的库、入库必须写明价值程度 / 动机用途计划 / 自己的概率估计。启用 Lean 时另有本所 Formal/(工作文件 + 索引 + 形式化待办)与 Verified/Lean/(归档证明),以及跨项目的 <VibeMath根>/Formal/{Lib,Proved}/——详见上方「Lean 形式化验证」一节。


⚡ 5 分钟上手

一条主线:说人话启动 → 随时问进度 →(可选)调参 / 干预 → 收尾。收口时四个预设会默认自动产出一篇最终论文(Paper/<id>/,见上「功能特色」与 docs/final-paper.md)。下面三种用法任选,不必都读。

方式 A:直接对话(推荐,最省事)

因为主代理内置了使用说明,你直接说人话即可:

帮我用 Vibe Math 证明 √2 是无理数。

主代理会自动:vibe_math_add_problem 加题 → vibe_math_start 启动 → 之后你随时问它进度。

现在进展怎么样了?

主代理会自动调用 vibe_math_status / vibe_math_report 并把结果用人话汇报给你。

方式 B:命令 / 工具(精确控制)

在对话里直接调用工具(参数为 JSON):

工具 作用
vibe_math_add_problem 加题(id/description/priority/dependencies?;v3 生成 Problems/<id>.md)
vibe_math_add_proposition / vibe_math_list_propositions(v2/v3) 添加 / 列出命题库(id/概述/布尔估计/细类型/价值·关键性;v3 生成 Propos/<分类>/<id>.md)
vibe_math_start / vibe_math_resume 启动 / 断点恢复调度器
vibe_math_pause / vibe_math_abort 暂停 / 终止(中断所有子代理)
vibe_math_status / vibe_math_report 查看状态 / 完整进度报告
vibe_math_set_mode 切换 auto / manual
vibe_math_set_params 运行时调参
vibe_math_setup 返回参数 schema(交互式配置用)
vibe_math_save_settings 把当前参数存成新默认
vibe_math_template 生成默认参数模板文件
vibe_math_new_project / vibe_math_set_project / vibe_math_list_projects 项目管理
vibe_math_list_decisions / decide 查看 / 裁决人工决策(v3:node=plan 计划审批 / node=method-promote 方法晋升)
vibe_math_list_agents / vibe_math_message_agent / vibe_math_interrupt_agent 查看 / 发消息 / 中断子代理
vibe_math_plan(v3) 查看待执行计划 / 上次计划,或 force:true 强制触发一次规划
vibe_math_index(v3) 从 md 知识库重建机器索引(State/index.json)
vibe_math_method_add / vibe_math_method_list(v3) 手动添加 / 列出方法卡(项目 + 全局)
vibe_math_lock_status(v3) 查看项目锁占用
vibe_math_claim_write / vibe_math_release_write(v3) 申请 / 释放某个 md 文件的写锁(代理直接写文件前调用;同一文件同一时刻只允许一个代理写,防并发冲突)
vibe_math_sync_meta(v3) 代理把内容写进 md 后上报轻量元数据(方向状态/存活率/引理 id/方法卡 id/新发明),让调度器同步索引——内容留在 md,不进 JSON

斜杠命令(与工具等价):/vibe start|resume|pause|abort|status|report|mode <auto|manual>|setup|save|template [global|project]|add <id> <desc>|add-proposition <id> <概述>|list-propositions|project [list|new <name>|<name>]|decisions|agents(v3 另有 methods|index|plan|lock)

🎓 让主代理替你干活(不用记命令)

1. 自然语言驱动(不用记命令)

主代理的作用就是当你的「翻译官」。你只需描述目标,它会自己选择并调用工具:

你说的话 主代理做的事
“求解 / 证明 XXX” add_problem + start,之后汇报
“现在进度怎么样 / 有哪些代理在跑” status / report / list_agents 并总结
“暂停 / 终止求解” pause / abort
“切到人工模式,我要逐步把关” set_mode manual,之后有决策就 list_decisions 提醒你
“给 q1 的某个求解方向换个思路(比如改成构造性证明)” list_agents 找到 childId → message_agent 注入新指令
“中断某个卡住的子代理” interrupt_agent

2. 问答式参数配置(/vibe setup)

你甚至不用记参数名。说:

帮我配置一下参数。

主代理会调用 vibe_math_setup 拿到完整参数 schema(每项含说明 / 选项 / 建议 / 当前值), 然后用 ask_user_question 逐项问你(选项自带解释与建议),你选完它用 vibe_math_set_params 应用,最后问你是否 vibe_math_save_settings 存为默认。

也可以直接跑命令:/vibe setup(看 schema)→ 跟主代理说你要改哪些 → /vibe save(存默认)。

3. 配置文件(vibe_math_setting.json)

  • 生成模板:/vibe template(生成到工作区)或 /vibe template project(生成到当前项目)—— 会产出一份带 // 注释、逐项中文说明的 JSON 模板,你手改后重启/resume 即生效。
  • 保存当前值:/vibe save 把当前生效参数写回该文件。
  • 唯一持久化来源:该文件是参数的唯一持久化层(项目级优先 → 缺失时回退全局 <工作区>/VibeMath/vibe_math_setting.json → 内置默认)。 vibe_math_set_params / set_mode 会立即写回项目级文件并持久化,无需再手动 save。

🌱 完整示例:证明 √2 是无理数

Step 1 — 用一句话启动

帮我用 Vibe Math 证明:√2 是无理数。

主代理执行 vibe_math_add_problem {"id":"q1","description":"证明:√2 是无理数。","priority":0} 再执行 vibe_math_start,然后告诉你“已启动”。

Step 2 — 询问进度

进展如何?

主代理执行 vibe_math_status 并用人话汇报:当前活跃子代理数、正在验证的单元、是否有待决策等。

Step 3 — 问答式调参(可选)

我想让它用强制裁决模式(forced)跑,并发数设成 6。

主代理 vibe_math_set_params {"verdictMode":"forced","maxParallelThreshold":6}, 并问你是否 vibe_math_save_settings 保存。(verdictMode 只接受 flat|forced;写其它值不报错,会被静默回退成该架构的默认值——v2 是 flat、v3 是 forced。)

Step 4 — 中途干预(可选)

切到人工模式,我要在每个关键节点把关。

主代理 vibe_math_set_mode {"mode":"manual"}。之后每到一个关键节点它会 vibe_math_list_decisions 拿到决策,向你说明,等你 vibe_math_decide {"id":"...","action":"approve"}(或 reject / override)。

Step 5 — 收尾

结束了吗?结论是什么?

主代理 vibe_math_status:qs/qs.json 里 q1 已回写 已解决 = true,其解法 正确概率 = 1;定论事实进入 Verified/<分类>_Verified.json。

v2 不写 CSV:已解决问题就在 qs/qs.json 里,Verified/<分类>_Verified.json 是定论事实索引(解法 正确概率 = 1 → 问题收口;证明/证伪 正确概率 = 1 → 命题布尔估计 = 1/0)。

Step 6 — 收口时自动产出最终论文(默认开启)

四个预设默认 finalPaper=true:论文阶段在各个收口信号命中后、run 被标记完成之前启动(v2/v3 由专职「论文撰写」子代理整理已有证据,v4/v5 由团队合写 → 交叉互审 → 定稿代表定稿并取得一致认同)。产物在 Paper/<id>/{paper.md,paper.tex,paper.pdf,paper.meta.json,paper.log.md}:paper.tex / paper.pdf 只在 paperFormat 含 tex 且宿主检测到 LaTeX 引擎时产出(中文优先 xelatex;没有引擎就只交 md/tex,不阻塞收尾)。手动触发用 /vibe paper(v2/v3)、/v4 paper、/v5 paper,可带 lang= / format= / editor= / force;完整契约见 docs/final-paper.md。

🖼️ 实际使用示例(长截图)

截图很长,这里默认折叠:点击下方「展开」才加载整张长图,避免它占满页面、遮挡前后文字。

📸 展开查看实际使用示例长截图

实际使用示例长截图


⚙️ 参数速查表

共用参数(被 ≥2 个预设接受)

每个预设的完整参数集 = 本表「适用」列含该预设的每一行 ∪ 该预设的专属参数表(v2 没有专属参数)。 参数细节与门禁位置另见 docs/formal-verification.md 与 docs/final-paper.md。

参数 默认 适用 说明(含各预设差异)
mode auto v2·v3 auto / manual(manual 在关键节点挂起决策等你 approve/reject/override)
maxParallelThreshold 4 v2·v3 全局最大并发子代理轮数(新派发前须 active < 阈值)
solverMaxRounds 3 v2·v3 每个求解方向最大迭代轮数(agent_self_iteration 上限)
directionsPerSolver 1 v2·v3 每个 solver 提示词可见的方向总数(1 = 只看自己方向、互不干扰;N>1 = 自己 + 最多 N-1 个其他活跃方向摘要)
verifierCount 3 v2·v3 每个验证对象的独立验证器数量
debateMaxRounds 5 v2·v3 验证辩论(交流群)最大轮数
verdictMode v2 flat;v3 forced v2·v3 默认按预设不同。 v2 flat = 取各验证者报告概率的等权平均(不一致时不再一律判 0.5);v2 forced = 强制裁决(按历史准确率+严谨性加权;准确率按模型追踪,且只在对象此后获得布尔裁决时计分)。v3 forced = 先做近共识判定(全部结果同侧且均值 ≥0.85/≤0.15 取均值——先于模式生效,所以 0.9 vs 1 在两种模式下都得到 ≈0.95),否则取各验证者概率的等权平均(不再按准确率加权;严格的 1/0 仍以绝对票生效),flat 则判 0.5(不一致即不确定)
reportMode file v2·v3 file = 写报告文件 / push = 推送主代理汇报 / both
promoteValueThreshold 0.7 v2·v3 Propos 中「价值/关键性」≥ 该值且未决(0,1) 的命题自动加入 qs.json
priorityAdjust none v2·v3 none / deadend-deprioritize(全死路降优先级)/ survival-map(按存活率重算)
proposPriorityAdjust none v2·v3 命题优先级动态调整:none / progress-graded(按定论接近度+证明/证伪材料量重算,越接近定论越优先验证)
provider / model 空 四套 模型路由(空 = 继承根代理)。各预设语义:v2/v3 = 子代理模型(v3 的规划代理另见专属表 plannerProvider/plannerModel);v4 = 常驻 LLM 路由(此前声明未用,v1.4.1 真正接入);v5 = 成员 LLM 路由(空 = 继承所办/主代理路由)
solverPersona / verifierPersona / explorerPersona 空 v2·v3 注入求解器/验证器/explorer 提示词开头的人格/要求
knowledgeContext 空 v2·v3 共享知识/数据模型说明(空 = 内置完整版:对象/属性定义、概率语义、文件夹用途、输出完整性要求;非空 = 覆盖并注入所有子代理提示词)
solverToolAllow / solverToolDeny [] v2·v3 求解器允许/禁止的工具
verifierToolAllow / verifierToolDeny [] v2·v3 验证器允许/禁止的工具
solverAllowNetwork / verifierAllowNetwork 空 v2·v3 网络工具开关(web_search/web/fetch):空=继承全部;true=在已有 allow 列表时补入;false=禁止
solverAllowScripts / verifierAllowScripts 空 v2·v3 脚本工具开关(bash/pwsh):同上
solverMaxToolCalls / verifierMaxToolCalls 0 v2·v3 每轮外部工具调用上限(0=不限)
reportIntervalMs 0 v2·v3 0 = 仅事件驱动(有状态更新才写/推);>0 = 定时自动汇报(毫秒)
mathComputation auto 四套 数学计算工具档位:off(真 no-op,不探测/不执行/不进提示词)/ auto(探测到引擎才工作)/ on。详见 docs/math-computation.md
mathMode typed+shell 四套 提示词策略(插件无法强制):typed+shell 允许工具不可用时用宿主 shell 兜底,但结论必须标注"未经工具归档"、只有工具路径算可复核支撑材料;typed 不提 shell 且禁用 engine:'cli'
mathEngines [python, r, octave, julia, matlab, maple, wolfram, cli] 四套 允许的引擎及探测顺序。商业三家(matlab/maple/wolfram)只探测与许可检查、永不安装;去掉 cli 即关闭通用逃生口
mathTimeoutMs 60000 四套 单次计算上限(毫秒,最小 1000);超时后主动终止进程
mathPackages [] 四套 默认要求存在的包/工具箱;缺包只报告并给安装计划,不自动安装
mathInstallScope user 四套 安装作用域;system 必须每次显式指定且不被记住(多数包管理器没有 system 模板,此时会被拒绝)

归档即证据:每次计算都写出 Computation/<id>/,回执含 scriptPath 与 scriptHash;脚本原件可以打开/编辑,编辑后必须用 mode:'file' 重跑得到新回执——旧回执不代表修改后的代码(scriptChanged / scriptChangedDuringRun 会显式告警)。归档只追加不覆盖,超上限只告警不删除。详见 docs/math-computation.md §4.1。

替代必须声明:当替代方案改变精确性或结论强度(精确解→数值近似、闭式解→采样/求积、改精度/容差/假设、换算法类)时,结论必须写明,不得像得到了原本的结果;拿不到精确结果就直说(规则行 MATH_SUBSTITUTION_RULE_LINE,已注入四套 persona 与提示词)。

安装与版本:op:'install' 按检测到的 python 环境分派 conda/mamba(-c conda-forge)、uv(uv pip …)或 pip 回退(歧义时标 managerAssumed);R/Octave/Julia 只做用户级(system ⇒ MATH_REFUSED + 每引擎理由)。版本求解交给包管理器:本工具只按 base name 查存在、把 pkg==1.2(conda pkg=1.2)原样透传,危险或不认识的写法 ⇒ unsupported-version-syntax。详见 docs/math-computation.md §5.1–5.3。 | tickIntervalMs | 2000 | v2·v3 | 调度器心跳间隔(毫秒) | | activityLogCap | 100 | v2·v3 | 活动日志保留条数(report 最多显示 30 条) | | maxExplorerRetries | 3 | v2·v3 | explorer 拆方向失败的重派生上限 | | maxParallel | 3 | v4·v5 | 同时唤醒的常驻(v4)/成员(v5)上限(框架侧并发闸,非指派) | | activityTimeoutMs | 120000 | v4·v5 | v4:空闲心跳间隔(超时才触发自驱动 CHECKPOINT 唤醒,推动常驻继续推进;唤醒失败会自动重新武装心跳,保证小组永不永久停死);v5:空闲兜底心跳间隔(主驱动是一次性活动等待,不轮询;任务板的"推一把"也按它节流) | | stallAutoMeetingMs | 360000 | v4·v5 | 停滞自动同步会议阈值(分级保活 B):团队空闲且无新产物超过该时长时,框架自动召集一次同步会议,让成员自行决定下一步路线/分工(框架只促成,不指派) | | verdictMaxRounds | 3 | v4·v5 | 验证在独立初评后进入辩论(v4)/公开辩论(v5)的最大轮数 | | compactThreshold | 66 | v4·v5 | 上下文占比(0–100)达此值触发软压缩:v4 = 常驻上下文占比达此值触发软压缩(自述指令);v5 = 成员达此值触发压缩(把工作状态浓缩进 Progress/) | | compactAfterRounds | 8 | v4·v5 | 每累计 N 轮(未压缩)触发一次软压缩 | | meetingKeepEvery | 5 | v4·v5 | 每积累 N 个新产物自动触发一次同步会议 | | toolAllow / toolDeny | [] | v4·v5 | 常驻/常驻员工工具权限(经 startContinuable 的 toolFilter 做作用域 tools.restrict();空 = 继承全部工具;⚠️ 空 allow:[] 会拒绝一切工具);v5 的临时工另有专属 tempToolAllow/tempToolDeny | | formalVerify | 'off' | 四套 | Lean 形式化验证开关:'off' 不额外要求(默认)|'encourage' 鼓励(验证时按实现难度自行决定是否形式化)|'require' 强制(真/假结论必须先有「Lean 通过」或显式阻塞记录,否则记为未定论并进入形式化待办)。非法值一律回退 'off' | | leanCommand | 'lean' | 四套 | 要执行的 Lean 可执行文件(例:'lake') | | leanArgs | [] | 四套 | 插在文件名之前的附加参数(例:['env','lean'] 配合 leanCommand='lake') | | leanTimeoutMs | 120000 | 四套 | 单次 Lean 运行的上限(毫秒)(异步作业同样用它作单次预算) | | leanAsync | true | 四套 | Lean 编译模式:true(默认)= 后台队列,lean_run / lean_archive{run:true} 入队即返回 async.jobId,成员不阻塞;false = 同步 await(旧语义逐字保留) | | leanJobsMaxParallel | 1 | 四套 | 后台编译并发上限(默认 1 = 串行;调大即并行) | | leanInitiative | 'normal' | 四套 | 日常形式化主动性:off / normal(默认,顺手形式化)/ eager(更主动)。与 formalVerify(验证时的要求强度)是两件事 | | leanSearchPaths | [] | 四套 | 额外 Lean 搜索根(先注入它们、再注入自动的 <VibeMath 根>;leanArgs 里已有 --search-path/-R/--root 时不注入) | | finalPaper | true | 四套 | 最终论文:收口时自动撰写(false 只关自动触发,手动命令仍可用)。完整契约见 docs/final-paper.md | | paperFormat | both | 四套 | 论文产出格式:both(md+tex)/ md(跳过编译,且不报"缺 tex")/ tex | | paperLanguage | zh | 四套 | 论文语言:zh(ctexart,引擎优先 xelatex)/ en(article,pdflatex 优先) | | paperCompilePdf | true | 四套 | 检测到 LaTeX 时编译 paper.pdf;无引擎或编译失败则保留 tex+md 并记日志告警 | | paperLatexCommand | '' | 四套 | 指定 LaTeX 引擎可执行文件(空 = 按语言自动探测 xelatex→latexmk→pdflatex→lualatex→tectonic) | | paperEditor | v4 office;v5 academician | v4·v5 | 定稿代表。v4:office(会话根/人类侧,默认)或 resident:<id>(该 resident 已离职则降级 office 并在 meta/log 记明);v5:academician(默认,无人值守也能完成)或 office(仅手动 /v5 paper editor=office,须先与全所交流 + 开会) |

  • 异步是默认:leanAsync=true 时编译在后台队列里跑,lean_run / lean_archive{run:true} 立即返回;leanAsync=false 才回到同步等待。
  • 只有"落地为通过"才算通过:作业必须 settled 且 exit 0,并且编译期间文件内容哈希与构建上下文都没变,才置 passed / 写 Verified/Lean/<id>.lean;其余(排队 / 失败 / 超时 / 中断 / 内容或上下文已变)一律停在 attempted。

v2(概率驱动 · 经典)专属参数

v2 没有专属参数:它的完整参数集就是上表「适用」列含 v2 的每一行。运行时用 vibe_math_set_params(或 /vibe set)调整,持久化在项目级 vibe_math_setting.json(缺失时回退全局 <工作区>/VibeMath/vibe_math_setting.json → 内置默认)。

最终论文(final paper)

四个预设都默认开启:收口判定命中后、在 run 被标记完成之前进入 paper 阶段。v2 由一名专职「论文撰写」子代理把已定论证据整理成 Paper/<项目>/{paper.md,paper.tex,paper.meta.json,paper.log.md}(检测到引擎时才有 paper.pdf)。手动:/vibe paper [lang=zh|en] [format=both|md|tex] [force]。PDF 需要宿主上有 LaTeX 引擎(中文优先 xelatex);没有引擎或编译失败时 tex+md 照常交付,只记日志告警——不阻塞定稿、不覆盖已有 pdf。完整契约见 docs/final-paper.md。

v3(论文式 md + 规划代理 + 方法库)专属参数

v3 接受 v2 的全部参数(见上表「适用」列含 v3 的行),并新增:

参数 默认 说明
planningHorizon 3 规划代理一次计划的最多动作数("接下来 n 次")
plannerEnabled true false = 完全走内置启发式调度(规划代理禁用)
plannerProvider / plannerModel 空 规划代理模型路由(空 = 继承根代理)
plannerPersona 空 注入规划代理提示词开头的人格/要求
planMinIntervalMs 30000 两次规划调用的最小间隔(毫秒);对每一次规划调用都生效(含空计划、含"空闲但仍有工作",不再有空闲绕过)
plannerMaxFails 3 规划代理连续失败达此值 → 自动降级启发式
methodKeepIntervalMs 0 Method Keeper 定时整理间隔(0 = 事件驱动)
methodKeepEvery 5 每积累 N 个待沉淀发明/新命题触发一次整理
methodAutoPromote false 项目级方法自动晋升全局库(false = 人工门)
indexAutoRebuild true 每次写盘后自动重建 State/index.json(false = 手动 vibe_math_index)
projectLockTimeoutMs 60000 项目锁等待超时(同项目同一时刻只允许一个会话调度)
methodKeeperPersona 空 注入方法整理代理提示词开头的人格/要求

最终论文(final paper)

v3 与 v2 同一开关、同一时序(严格收口;在调度器停止之前派遣撰写者):专职「论文撰写」子代理产出 Paper/<项目>/{paper.md,paper.tex,paper.meta.json,paper.log.md}(检测到引擎时才有 paper.pdf)。手动:/vibe paper [lang=zh|en] [format=both|md|tex] [force]。无引擎或编译失败仍交付 tex+md、记警告、不阻塞定稿。完整契约见 docs/final-paper.md。

v4(常驻自组织 · 实验)专属参数

vibe_v4_set 可调(持久化到 State/settings.json);共用参数见上表,v4 另有:

参数 默认 说明
residentCount 4 常驻数(可 vibe_v4_add_member 增减)
residentPersona 空 注入每个常驻提示词开头的人格/要求

最终论文(final paper)

默认开启;v4 在一致性会议投出「一致停止」票后、标记完成之前进入 paper 阶段。团队流程:各 resident 写自己库里的部分 → 合并(去重、统一术语与记号)→ 至少一轮交叉互审 → 定稿代表按 paperEditor(默认 office,或 resident:<id>)梳理成最终稿 → **全体明确"可交付"**才定稿(有反对则继续迭代,超轮次上限记警告并把分歧写进附录)。手动:/v4 paper [lang=] [format=] [editor=office|resident:<id>] [force]。产物 Paper/<run id>/{paper.md,paper.tex,paper.meta.json,paper.log.md,paper.lock.json}(引擎可用时另有 paper.pdf;paper.lock.json 是该目录的写锁,用于并发的复写/重编译串行化)。完整契约见 docs/final-paper.md。

v4 专属工具 vibe_v4_formal_report(文档补记,round-3):把"哪些命题/方法已经得到形式化支撑、支撑强度如何"汇报给常驻团队,是 v4 团队自治流程的一部分——居民之间要靠这条汇报对齐"谁能引用哪条已定论结论",因此它只存在于 v4(v2/v3 是专职求解/验证子代理架构,其形式化状态由 vibe_math_lean_* 与验证日志承载;v5 由院士评审路径 vibe_v5_propose_verify/vibe_v5_verdict 与 vibe_v5_status 承载)。v4 的两处 persona 文本块都要求成员使用它;v4 的 status/report 也会汇总其输出。

状态面不对称(文档补记,round-3):v2/v3 的 vibe_math_status 返回参数块(含 math*/lean* 现值),而 v4 的 vibe_v4_status 与 v5 的 vibe_v5_status 返回各自的状态/成员/研究所视图但不含参数块(参数请用 vibe_v4_set/vibe_v5_set 的 schema 或对应 status 里的既有字段)。这是既定设计(v4/v5 的参数面在 *_set 的闭合 schema 上),本轮选择在文档里声明而不是给 v4/v5 加参数块。

v5(研究所体系 · 实验)专属参数

vibe_v5_set 可调(持久化在研究所状态文件 State/<研究所>.v5state.json 里);共用参数见上表,v5 另有:

参数 默认 说明
academician true 是否设院士(1 名)
academicianLeads true 是否启用院士的组织/分派职权(关掉则退化为 v4 式纯自组织,只有所办能协调)
memberMayRejectAssign true 成员可否据理反对院士的分派(反对不阻塞执行,但理由会广播给院士与全所)
researcherCount 3 常驻研究员数(建所时)
quorumCap 3 m 的上限;实际 m = min(quorumCap, 在册有表决权人数)
quorumMode 'm-unanimous' v5 口径;切 'all-unanimous' 回到 v4 的"全体一致"
maxTempPerMember 3 每位院士/研究员同时在册的临时工上限(按在册计,非累计——所以换人不受限)
maxTempTotal 12 全所同时在册临时工上限
chatDigestMs / chatDigestMax 45000 / 12 群聊摘要合批的时间窗与条数上限(私信/会议/表决不合批)
tempToolAllow / tempToolDeny [] 临时工的工具权限(比常驻更窄)
staffPersona 空 追加到每个成员章程前的人格/要求

最终论文(final paper)

默认开启;v5 在 checkSolved 判定「已解决」后、标记完成之前进入 paper 阶段。常驻研究员与院士各自写、合并、交叉互审,定稿代表由 paperEditor 决定:自动流程固定用 academician(所办是根会话,没有唤醒路径);office 只能通过手动 /v5 paper editor=office 选择,此时所办必须先与全所交流、商讨、优化、审查(≥1 条 vibe_v5_message + ≥1 次 vibe_v5_meeting),把结论写进定稿说明,再调用 vibe_v5_finalize_paper;缺一即被拒(V5_PAPER_CONSULT_REQUIRED)。工具入口:vibe_v5_paper、vibe_v5_finalize_paper。产物 Paper/<研究所 id>/{paper.md,paper.tex,paper.meta.json,paper.log.md}(引擎可用时另有 paper.pdf)。完整契约见 docs/final-paper.md。

常用控制:vibe_v5_configure(先配置)→ vibe_v5_start(开工)→ vibe_v5_report / vibe_v5_status;vibe_v5_message / vibe_v5_meeting / vibe_v5_members / vibe_v5_hire / vibe_v5_fire(临时工)/ vibe_v5_add_researcher / vibe_v5_remove_researcher(增删常驻,仅所办)/ vibe_v5_pause / vibe_v5_resume / vibe_v5_stop;斜杠命令 /v5。


📝 断点续跑 & 人工干预(两大硬性需求)

  • 断点续跑:所有状态落盘(v2:VibeMath_State/*.json;v3:State/*.json;v5:研究所目录下的加固 JSON State/<研究所>.v5state.json),每个子代理都是 DSH 的 continuable 持久会话(对话由 DSH 自动保存)。重启后新开会话 → vibe_math_resume / vibe_v4_resume / vibe_v5_resume 即可续跑。v2/v3 额外用进程纪元区分"同进程暂停→恢复"(保留存活子代理继续)与"跨进程重启"(清理陈旧任务)。v3 的 md 知识库本身就是叙事断点——代理 resume 时从研究日志/问题卡/命题卡尾部续写;v5 由状态文件承担——恢复就是"读之前先 load",跨进程与同进程走同一条代码路径,成员会话重建时会以"读回你自己的 Progress/"重新种化(而不是让它们从头再来)。
  • 中途人工干预:manual 模式在关键节点挂起决策(v2:explorer/solver 派发、验证裁决;v3:计划审批门(规划代理产出计划后等你 approve/reject)、验证裁决门、方法晋升门(项目方法 → 全局库));可随时 set_mode auto 切回自动(自动放行所有挂起决策);可对任意子代理 message_agent / interrupt_agent。v4/v5 天然可干预:随时给成员留言(vibe_v5_message)、召集会议、暂停全所、增删编制——成员下一轮就会看到。
  • 进度汇报:默认事件驱动 —— 只有代理状态更新等事件发生时才会写报告(v2:Progress_Logs/report.json;v3:Progress_Logs/report.json + Logs/报告.md 论文式人读摘要;reportMode 可 file/push/both,push 通过 subagents.sendMessage(根代理, 常驻子代理, …) 唤醒常驻主动汇报——followup 不是 subagents 服务的方法,它只是 Agent 对象方法);只有把 reportIntervalMs 设为 >0 才启动定时自动汇报(间隔毫秒)。v4/v5 的工作汇报是"所内自述":成员把进展写进自己的 Progress/、把关键结论说进群聊(v5 另有人读镜像 Institutes.md / Shared/TaskBoard.md / 会议纪要 / 辩论录 / Problems/conclusion.md)。

📚 规格文档

  • v2(概率驱动):vibe-math-v2/实现方案.md
  • v3(论文式 md + 规划代理 + 方法库):vibe-math-v3/实现方案.md
  • v4(常驻自组织):vibe-math-v4/实现方案.md
  • v5(研究所体系):vibe-math-v5/实现方案.md(文字规格)· vibe-math-v5/架构图.md(全套架构图)
  • v5 提示词与交互语料:prompt-corpus-v5/prompt-corpus-v5.md(框架真正发出的每一条提示词原文,可直接人工复核身份/编制/交互署名是否正确)
  • 四套 Lean 提示词语料:prompt-corpus-v2/formal-verify-v2.md · prompt-corpus-v3/formal-verify-v3.md · prompt-corpus-v4/formal-verify-v4.md(各自覆盖 off / encourage / require / 忠实性分支 / 工作轮 / 回执契约;工作区归一化为 <WS>、VibeMath 根为 <VIBEMATH>)
  • 四个预设的 persona 原文:prompt-corpus-persona/persona-corpus.md(主代理实际收到的提示词:有哪些工具、哪些参数、哪些斜杠子命令;由 audit-persona-surface.test.mjs 生成,随包发布)
  • Lean 形式化验证(四架构共用契约):docs/formal-verification.md
  • 最终论文(四架构共用契约):docs/final-paper.md(五个参数与 v4/v5 的 paperEditor、收口顺序"先论文后完成"、Paper/<id>/ 产物与 9 节骨架、LaTeX 检测顺序与"先修复后降级"、v4/v5 团队合写流程与 v5 所办咨询规则)
  • 测试耗时基线与并行跑法:docs/test-timing.md(node tests/run-tests.mjs 并行跑全部套件 + 全部探针:TOTAL 57(39 套件 + 18 探针/变体)≈3.5 min;哪 18 项随包发布、哪些仅仓库见该文档 §1.1;每个 runner 都会打印耗时/加速比供下次选策略)
  • 静态提示词面一致性(persona ↔ 工具注册表 ↔ 斜杠命令 hint/usage):audit-persona-surface.test.mjs(260 条断言,并生成 prompt-corpus-persona/persona-corpus.md 供人工复核)+ audit-persona-sensitivity.mjs(16 条灵敏度探针)——守"注册的工具必须在 persona 里出现 / persona 里的名字必须真的注册 / prefix 与 text 两块逐行一致 / hint、usage、实际分支三处必须一致"
  • 全面检查必查清单:AUDIT-CHECKLIST.md(本仓库的强制审计流程;§1.9 专门查"工具参数 schema 收不收得下")
  • 提示词/交互不变式(四套一起,可一键复核):audit-prompt-invariants.mjs(157 条断言)——把"历史上真实发生过的提示词/工具面缺陷类别"逐条编码成静态不变式(缩写工具名、把忠实性缺陷投成 0、defect 只写在提示词里没实现、回执契约缺 defect、无 note 放行、字段名错、off 档回执仍能写状态、语料不确定、探针缺失、工具的封闭 schema 收不下它自己文档里的参数、schema 声明了参数层却静默丢弃的键)。加 --self-probe 会在内存里注入这些缺陷形状,要求对应不变式变红、未变异的对照跑仍为绿(5/5);脚本自身另带 X5–X8b 六条自检(注释扫描器必须认正则字面量——包括 return /…/ 这种关键字后面的正则——字符串里的 // 必须保留、抹注释不改变行结构,以及"四套源码抹掉注释后仍必须能被 node --check 解析"这条解析级判据)
  • 规格 ↔ 代码可追溯(四套一起):audit-spec-traceability.mjs(94 条断言)——实现方案.md/README 里承诺的工具必须真的注册;四个 Lean 参数必须同时被文档与代码接受
  • v5 静态完整性:audit-v5-integrity.mjs(≈0.5 s)——调用了但未定义的函数、未声明的 params.* 读取、会话 API 上不存在的方法、文档化但从未抛出的错误码、遗留开发标记,外加扫描器解析级自检(它先把注释/字符串/正则抹掉再扫描,自检保证"抹除后的源码仍能被 node --check 解析"——2.3.5 修掉的正是这个扫描器读错 30 行的盲区);配套 audit-v5-sensitivity.mjs(39 条探针,全红才算通过)

⚠️ 已知边界(有意简化)

v2:

  • (DSH ≤ 0.1.6 的目录形式) 安装器带版本化自动更新:每次 DSH 启动时对比包版本与 <presetRoot>/.vibe-math-installed.json 记录——版本一变(或无记录的老安装首次运行)就整体替换受管文件,不看它是否被改过;被替换的手改原文先备份到 <presetRoot>/.vibe-math-backup/<旧版本>/<preset>/ 并在日志里列出。同一个版本内不重写任何文件(重启 DSH 不会改写 preset、也不会扰动它按 mtime 记的生成代际),缺失文件随时补回。想强制全量重装:删除那四个 preset 目录后重启 DSH。 在 DSH ≥ 0.1.7 上安装器不写这些目录(预设由上文「安装」里的组合行提供),启动时只会提示旧副本可安全删除。
  • 在 DSH ≤ 0.1.6 上,这四个目录由安装器负责:删掉其中任一文件或整个目录,只会在下次启动 DSH 时被补回(这正是上面"强制全量重装"可行的原因)。在 DSH ≥ 0.1.7 上它们不再被读取、也不再被写入,直接删掉即可;想彻底不要本包的预设,就卸载本包(dsh plugin --profile <你的 profile> remove dsh-vibe-math)。
  • flat 裁决在辩论不一致时取各验证者概率的等权平均(不再直接判 0.5;早期把高置信分歧 0.9 vs 1 误判为 0.5 的问题已在 v2/v3 修复);forced 按历史准确率+严谨性加权,且准确率只在对象此后获得布尔裁决时计分。
  • never 优先级的问题/命题永不调度,且不阻塞严格终止(视为主动弃权)。
  • 四个 preset 文件互相独立、可共存;同一会话同时只能选一个预设。

v3:

  • 软规范而非零规范:md 知识库只强制对象头部的 4~7 行锚点(- ID/类型/状态/概率/优先级/依赖/...)与条目标题行(### 解法/证明/证伪 N|标题|概率X|状态Y),供调度器可靠索引;正文完全自由论文式叙述,调度器从不解析正文。手工编辑锚点可能导致索引漂移(调度器会保留上次有效索引并告警)。
  • 规划代理是增强而非必需:plannerEnabled=false 或规划代理连续失败(plannerMaxFails)时自动回退 v2 式启发式调度;planMinIntervalMs 冷却对每一次规划调用生效——包括空计划和"空闲但仍有工作"的情形(空闲不再绕过冷却,那正是规划代理每 tick 空转的放大器)。
  • 方法库可信分层:方法卡的 可信断言 只允许链接已进 Verified/ 的 ID;方法条目的其余内容(含未验证的策略/直觉/启发式)一律视为经验参考,不得当定理引用。
  • 项目锁:同一项目同一时刻只允许一个会话调度(第二个会话启动会提示"被会话 X 占用");锁在暂停/终止/全部解决时自动释放。
  • 近共识裁决:全部验证器结果同侧且均值 ≥0.85/≤0.15 时取均值(如 0.9 vs 1 → 0.95),否则 forced 取各票的等权平均、flat 判 0.5——修复了 v2 中"数学上正确但形式有瑕疵"的结论被误判为不确定的问题。

v5:

  • 框架绝不指派任务:这是设计上的硬边界,不是尚未实现的功能。任务的产生与分配属于所内自治 (院士拆解分派、成员自行认领),框架只提供任务板、消息与会议这些协调工具。
  • ≥ m 一致 ≠ 数学上已证明:门槛只保证"所内达成了一致判断",不保证结论真的正确。 求真的纵深靠成员自己的推导与辩论录留痕;未达门槛的对象会留库附平均概率,不会被强行判真判假。
  • 一致性门槛不是"少数服从多数":任何一张反向布尔票都阻塞定论,弃权既不帮真也不帮假。 因此在本口径下(m = min(quorumCap, 有表决权人数))只要有人投布尔票,门槛就等于"全部布尔票同向": 调低 quorumCap 只是把"至少几张布尔票"降到 m,不会让收敛更容易;要更严格可切 quorumMode: "all-unanimous"(它连弃权都不允许)。
  • 一个回合永不结束的成员不会被强行释放(与 v4 同一边界):心跳每次都会重新武装, 所以调度器不会永久冻结;需要人工介入时用 vibe_v5_fire(临时工)或所办增删编制。
  • 会议与验证严格互斥:一方进行中,另一方排队/暂存。因此"在会议上当场定论一个对象"会先排队, 等会议收口后再走完整的表决流程。
  • resume 后轮次计数从 1 重新计(内存态,仅用于节流与压缩提示);权威进度在成员自己的 Progress/。
  • 成员章程是入职快照:升级本包不会改写已在跑的研究所里成员的章程(它们仍用入职时冻结的版本)。 需要新章程就在新会话里重开一个研究所;状态文件与文件树无需迁移。
  • 安装器行为同 v2(在 DSH ≤ 0.1.6 的目录形式上:版本一变即整体替换受管文件并先备份原文,vibe-math-v5 目录同样受管; DSH ≥ 0.1.7 上安装器不写预设目录,预设由组合行提供)。
  • Lean 形式化需要宿主上有 Lean 工具链:框架不内置、不下载;没有工具链时三个 Lean 工具会如实返回 LEAN_NOT_FOUND,形式化代码仍可写下来归档,但无法执行验证。
  • require 模式的门禁是「搁置」而不是「卡死」:缺形式化的真/假结论会被记为未定论 + 进入形式化待办, 研究所继续推进(与「未达门槛留库附平均概率」同一取舍),不会被一个对象永久卡住。

📄 License

MIT

About

Vibe Mathematics —— 多代理数学问题求解与形式化验证框架

Topics

Resources

Security policy

Stars

34 stars

Watchers

1 watching

Forks

Releases

Packages

Contributors

Languages