ChongCyrus/Vibe-Mathematics

English | 中文

A set of agent presets running inside DeepSeek Harness (vibe-math-v2 / vibe-math-v3 / vibe-math-v4 / vibe-math-v5), which use multi-agent collaboration to automatically solve mathematical problems and perform multi-agent cross-verification of the conclusions. All four presets share the foundational capabilities of "checkpoint resume, mid-run manual intervention, progress reporting, and natural-language driving", but adopt four generations of different solving architectures: 💡 vibe-math-v2 and vibe-math-v3 are recommended at the same level — both are mature, usable, actively maintained recommended architectures; choose according to your actual needs (see "How to choose" below); vibe-math-v4 is the "resident self-organizing collaborative research" architecture, and vibe-math-v5 is the latest "institute system" (both are experimental).

• vibe-math-v2 (probability-driven · JSON data layer) ✅ Recommended: qs.json problem list + Propos/ proposition library + probability-driven scheduling + code heuristic scheduling;
• vibe-math-v3 (third generation · paper-style md + planner agent + method library) ✅ Recommended: all knowledge is stored and extended in Markdown paper/research-report form (Problems/ problem list + dependencies + source motivation, Progress/ research log, Propos/ proposition library, Methods/ general theory invention library, Verified/ absolutely trustworthy); before scheduling, the planner agent autonomously draws up a plan for the next N steps; theories/frameworks/tools/methods/ideas invented during solving are distilled by the Method Keeper into a reusable method system (as in inventing group theory or functional analysis).
• vibe-math-v4 (fourth generation · resident self-organizing collaborative research) 🧪 Experimental: a group of persistent resident subagents leave messages for one another + hold meetings, and autonomously decide all task arrangements (no central scheduler); each accumulates its own progress/proposition/method/subproblem libraries and consults the others; verification is written to Verified/ only when all residents agree (true or false), otherwise it remains in the library with a probability attached; when the context reaches a threshold it automatically /compacts; it stops only when all agree that the original problem has been solved.
• vibe-math-v5 (fifth generation · institute system) 🧪 Experimental · Latest: upgrades the residents into an institute — academicians (leaders / the organizing and coordinating center, responsible for decomposition and assignment, setting priorities, chairing meetings, and supervising progress) + resident researchers (with voting rights, able to autonomously hire/fire their own temp workers) + temp workers (no voting rights); it has a public charter, group chat and meetings, a compare-and-set task board, and real firing; a boolean agreement of ≥ m votes is required to write to Verified/ (opposing votes block, abstentions are not counted, and if the threshold is not met it remains in the library with an average probability attached); state is stored in host-only projection units of the session log, at zero token cost.

After installing this plugin package (or manually copying the presets), four agent presets appear in DSH's preset selector.

---

🧩 Architecture Diagrams (v2 + v3 + v4 + v5)

Static architecture diagrams; for the complete process description see the v1-era architecture notes (historical: the layout changed from v2 on) and the v5 detail diagrams (the full set of v5 detail diagrams); editable generation scripts: the Chinese v2/v3 posters come from the matplotlib scripts v2 / v3 (matplotlib → PNG); the English v2/v3 diagrams come from the zero-dependency Node scripts v2-en / v3-en (→ SVG); v4 / v5 (zero-dependency Node → SVG, node docs/generate_framework_diagram_v4.mjs; add --lang=en for 示例图/框架图-v4-en.svg). SVG is used from v4 onward: plain text, diff-friendly, crisp at any zoom; when PNG is needed, screenshot with a headless browser (the command is at the top of the generation script).

Vibe Math V2 (probability-driven · JSON data layer) ✅ Recommended

One-sentence pipeline: qs.json takes problems by priority → Explorer splits out directions (if all are dead ends, re-derive) → one Solver per direction iterates over multiple rounds (lemmas go into Propos/, solutions go back to qs.json, all probabilities <1) → the scheduler picks r (proposition / proposition+proof·disproof / problem+solution) and dispatches ≥3 verifiers for independent review → debate → ruling → at probability=1 it automatically closes out (problem solved, proposition 1/0, priority set to never); state is written to disk throughout, resume continues from the checkpoint, and reportMode can report by file/push/both.

Vibe Math V3 (paper-style md + planner agent + methods library) ✅ Recommended

One-sentence pipeline: all knowledge is stored and continued as Markdown papers/research reports (Problems/ problem list including dependencies and the source motivation of follow-up problems, Progress/ research log continued by direction and by round, Propos/ proposition library, Methods/ general theory invention library, Verified/ absolutely trustworthy) → before scheduling, the scheduler builds a state brief and calls the planner agent; the planner agent lays out the next N steps in one go (spawn solver/verifier/explorer/method-keeper, interrupt, promote, wait), which are executed after code validation (actions exceeding the concurrency limit are queued and consumed across ticks; a planning failure automatically falls back to the v2-style heuristic) → verifiers review independently → debate → near-consensus ruling (if on the same side and the mean is ≥0.85/≤0.15, take the mean, fixing v2's flat misjudgment) → at probability=1 it closes out and generates a Verified/ card → the solver's methods_used/new_inventions reports are distilled/refined into the methods library by the Method Keeper (which can form system hierarchies and be reused across projects).

Vibe Math V4 (resident self-organizing collaborative research) 🧪 Experimental

The SVG above is generated by a zero-dependency script: node docs/generate_framework_diagram_v4.mjs --lang=en (pure Node, no Python/matplotlib dependency; generation estimates text width, and any line overflowing its container raises a warning and exits with code 1).

One-sentence pipeline: initially N resident subagents are created (continuable, persistent context) which first brainstorm on their own and produce initial insights/directions → after that all task arrangements are decided autonomously by them leaving messages for each other + holding collective meetings (the framework only provides the message bus/meetings/task board/artifact persistence, and never assigns tasks); each resident persists valuable artifacts into its own Progress/<id>/, Propos/<id>/, Methods/<id>/, Subproblems/<id>/ libraries according to degree of value / planned motivation and use / its own probability estimate, and they can read each other's; verification is initiated by their own deliberation, and only when all residents agree (true or false) is it written to Verified/, otherwise it stays in the library with a probability attached; when a resident's context reaches a threshold (66% by default) it automatically /compacts; they stop only when all of them agree that the original problem is solved; residents can be manually intervened with/added/shut down at any time, and checkpoint resume is supported.

Note: V4 removes v3's central planner and deterministic roles (explorer/solver/verifier/planner/method-keeper) and makes the "researcher" itself the subject. See vibe-math-v4/实现方案.md for details. Keep-alive mechanism (tiered keep-alive A+B + deadlock watchdog): a gang idle for longer than activityTimeoutMs receives a self-driven CHECKPOINT (suggesting it continue solving/send a message/propose a task, rather than "do you want to stop"), and it fills in parallel — branch A fills as much of the maxParallel concurrency budget as possible in one go (waking several idle residents at the same moment, rather than the serial "wake only r1, then r2 after it finishes"), and mailbox delivery also reaches several idle recipients in parallel; a failed wake automatically re-arms the heartbeat; if the team is idle and has no new artifacts for longer than stallAutoMeetingMs (6 minutes by default), the framework automatically convenes a synchronous meeting so the residents can decide the next step themselves; if a meeting/verification hangs (still no new speech/votes after more than 2×activityTimeoutMs), the framework automatically abandons that meeting/verification and returns to normal self-organization, so that one broken meeting does not permanently block the whole team; meetings do not preempt verification — meeting requests while verification is under way are held and convened afterwards (keeping the consensus-consistent "truth-seeking" step from being interrupted by coordination discussion) — the framework always only facilitates and never assigns tasks.

---

Vibe Math V5 (institute system) 🧪 Experimental · Latest

One-sentence positioning: upgrade v4's "a group of residents messaging each other" into an institute — with three classes of staff: academician (leader), resident researcher, and temp worker; with the institute's public charter; with group chat and meetings; with autonomous hiring/firing; and where any conclusion must be given a Boolean probability of 1 or 0 unanimously by at least m voting members before it can be written to Verified/.

Image sources and all detail diagrams (member lifecycle, one-round sequence, consensus state machine, meeting flow, scheduling priority, state folding, prompt composition, task board, authority matrix): the v5 detail diagrams. The SVG above is generated by a zero-dependency script: node docs/generate_framework_diagram_v5.mjs --lang=en.

flowchart TB
    OFF["👤 Institute office (session root agent / human)<br/>does not research · does not vote · only reports and relays instructions"]
    subgraph INST["🏛️ Institute (internal autonomy: roster, organization and assignment all happen among members)"]
        ACAD["Academician acad —— leader / center of organization and coordination<br/>L1 institute-wide overview · L2 assignment · L3 priority<br/>L4 chairs meetings · L5 supervision · L6 moving people · L7 external"]
        RES["Resident researcher r-n<br/>has voting rights · may autonomously hire/fire its own temp workers"]
        TMP["Temp worker t-n<br/>no voting rights · hired temporarily for a specific task"]
    end
    subgraph FW["⚙️ Framework vibe-v5 —— only a medium (middleware), never assigns tasks"]
        M["Message relay · meetings/debates · task board CAS+DAG<br/>m-vote consensus verification · context and liveness · roster and hiring · scheduler"]
    end
    PROJ["💾 host-only session log projection cell (key vibeMathV5)<br/>11 kinds of events · pure fold applyV5Event · DSH handles checkpoint/restore"]
    FS["📁 Members/&lt;id&gt;/* · Shared/* · Verified/ · Problems/"]
    RULE{{"Truth gate: Boolean unanimity and Boolean votes ≥ m = min(quorumCap, number of registered voting members)"}}
    OFF <-->|"vibe_v5_* / /v5 commands　↔　status / report"| M
    M <-->|"per-round prompt　↔　single JSON receipt"| ACAD
    M <-->|"per-round prompt　↔　single JSON receipt"| RES
    M <-->|"per-round prompt　↔　single JSON receipt"| TMP
    ACAD -.->|"assign / supervise / chair meetings (in-institute organization, not framework behavior)"| RES
    ACAD -.-> TMP
    M <--> PROJ
    M <--> FS
    M --> RULE

Positions and Authority

Position	Codename	Voting right	Authority
Academician (leader)	acad	✅ one vote, of equal weight with others	Center of organization and coordination: build an institute-wide overview (overview), decompose the original problem into tasks and assign them (assign), set priorities (prioritize), convene and chair meetings (convene), supervise progress (nudge), move temp workers around, report outward. Cannot unilaterally conclude, and cannot expand the roster on its own.
Resident researcher	r-<n>	✅ one vote	Digs deep in its own direction; may autonomously hire/fire its own temp workers; reports progress to the academician and accepts its organization and assignments (has the right of reasoned objection).
Temp worker	t-<n>	❌	Hired temporarily for a specific task: can read/think/speak/write its own output library/claim or be assigned tasks; fired by its employer or the academician. Codenames are never reused.
Institute office (main assistant)	——	❌	Does not take part in research and does not vote. Only reports, translates the human's words into tool calls, and holds on the human's behalf the creation rights the platform requires (creating an institute / adding resident researchers).

Division of labor in one sentence: organization is the academician's responsibility, but judgment belongs to each person individually —— what the academician assigns is work, not conclusions.

Truth Rules (the core of V5)

For an object to enter Verified/ it must simultaneously satisfy:

1. At least m = min(quorumCap, number of registered voting members) voting members cast a Boolean probability value;
2. These votes are all 1 (absolutely true) or all 0 (absolutely false).

A vote is a numeric value in [0,1]: strictly between 0 and 1 = abstention/doubt (not counted toward m, but counted in the group's average probability). Any single opposing Boolean vote blocks a conclusion —— the minority cannot push a conclusion through by having others abstain. An object that falls short of the threshold stays in its original library, with the group's average probability and the complete debate record attached, and is not forcibly ruled on.

Voting has two stages: first [independent initial assessment] (mutually invisible), and if undecided, then [open debate] followed by a re-vote, with a round cap of verdictMaxRounds. quorumMode: "all-unanimous" switches back to v4's "all-unanimous" standard.

Operating Mechanisms

• Communication: group chat (fanned out to every other member), direct message, votes cast only to members with voting rights; messages are persisted per recipient, written to disk before delivery, and group chat is batched into digests by chatDigestMs / chatDigestMax (direct messages/meetings/votes are not batched). All in-institute communication goes through the framework relay (DSH's adjacency restriction does not allow members to message each other directly), but the signature is always the real sender.
• Meetings and verification are mutually exclusive (in both directions): meeting requests while verification is under way are held; verification requested while a meeting is under way is queued —— the two consensus processes never run at the same time, avoiding mutual starvation of the watchdog clocks. Meetings collect opinions one by one in a random speaking order, and at closing they aggregate the votes and check whether everyone considers the problem solved.
• Task board: compare-and-set (the latest expected_revision must be read before a change) + dependency DAG (all dependencies must be complete before claiming; cycle detection rejects bad dependencies) + write-scope overlap warnings; when an owner is fired, its tasks are automatically reclaimed.
• Hiring / firing: both academicians and resident researchers can hire their own temp workers, with a dual quota per member (maxTempPerMember) and institute-wide (maxTempTotal); firing is real —— it cancels in-flight turns, releases the resident sub-session, reclaims tasks, and discards undelivered mail.
• Liveness: the main drive is a one-shot activity wait (vibe_v5_wait, no polling); the scheduler advances by priority (in-progress meetings/verification → queued verification → held meetings → active tasks → urgent mail → group chat digest → auto-meeting on stall → fallback heartbeat), and concurrency is gated by maxParallel; the task board's "nudge" is throttled by activityTimeoutMs.
• Watchdog: if a meeting/verification goes beyond 2×activityTimeoutMs with no new speech/new votes → abandon it and return to self-organization; the heartbeat is re-armed after every wake, so the scheduler never freezes permanently.
• Context: upon reaching compactThreshold (%) or accumulating compactAfterRounds rounds, members are asked to condense their working state into Progress/; the charter lives in the persona, remains in effect after compaction, and does not need to be restated every round.
• Stopping: the problem is concluded (writing Problems/conclusion.md) only when all voting members consider the original problem solved.

State and Persistence

Institute state lives in a host-only projection cell of the session log (key vibeMathV5): the framework's only side effect is appending 11 kinds of events to the session log, from which applyV5Event purely folds out the state. Therefore

• Zero token cost: these events do not enter the model context and do not consume members' conversation budget;
• Recovery takes the same code path: both cross-process restarts and resume after an in-process abort are covered by DSH's checkpoint/restore;
• the whole class of problems caused by v4's direct writes to State/*.json — "corrupted silent overwrite / concurrent lost writes / stale cross-process snapshots" — is eliminated by construction.

If the host has no sessionProjections service, v5 automatically falls back to hardened JSON (State/<institute>.v5state.json, the same fold, serial writes, and a mandatory load before read), and the installer's startup self-check reports this degradation. Files outside the projection (member output libraries, group chat, meeting minutes, debate records, roster mirror, task board mirror) are all human-readable artifacts, and breaking them by hand does not damage the institute.

How the Prompt Is Composed

A member's "persona" carries the ten-section public charter (roster and colleagues, general rules, knowledge base and progress format, organization and coordination, voting rules, per-round rhythm, hiring and firing, task board, context discipline, stopping conditions), which is frozen at onboarding and persists with the session; each round's prompt carries only a short state block (who I am / the round / m / the registered roster / my tasks / newly arrived messages), this round's question, and the receipt contract. Every field in the receipt contract that the framework actually handles appears, trimmed by position (temp workers have no verdict/hire/fire; non-academicians have no assign/prioritize/nudge/convene_meeting).

The framework treats "the text a member reads" as a product to be guaranteed: identity is passed explicitly and never guessed; a member is written to the roster first, and only then are its onboarding prompts constructed; the charter snapshot is frozen at onboarding, and a session rebuild is framed as the literal marker 【会话重建 —— <role> <id>】 ("session rebuild") rather than "just onboarded"; no academician narrative appears when there is no academician; message headers are labeled by true origin (institute office assignment ≠ academician assignment; supervision ≠ assignment); framework feedback has its own sender, and only one message is delivered per prompt.

Directory Structure (Institute)

<session workspace>/VibeMath/Projects/<project>/Institutes/<institute>/
├─ Institutes.md                 # roster mirror (human-readable snapshot, do not edit by hand)
├─ Problems/<id>.md              # original problem
├─ Problems/conclusion.md        # conclusion record
├─ Members/<codename>/
│   ├─ Progress/progress.md      # research log (the main basis for restoring state after compaction)
│   ├─ Propos/<id>.md            # proposition
│   ├─ Methods/<id>.md           # method / theory / tool
│   └─ Subproblems/<id>.md       # subproblem
├─ Shared/
│   ├─ Chat/<date>.md            # group chat log
│   ├─ Meetings/<mt-id>.md       # meeting minutes (including the voting section)
│   ├─ Debates/<object>.md       # debate record (each round's votes and reasons + average probability)
│   ├─ TaskBoard.md              # task board mirror
│   └─ State-of-institute.md     # snapshot of members' judgment on "whether it is solved"
├─ Verified/<type>/<id>.md       # conclusion (read-only; only this can be treated as established)
└─ State/README.md               # explains that "the authoritative state is in the session log projection, not here"

Tool Surface

Who	Tools
Institute office / human	vibe_v5_configure (configure first) → vibe_v5_start (start work); vibe_v5_resume / pause / stop; vibe_v5_set (adjust parameters, effective immediately); vibe_v5_status / report / members; vibe_v5_message / meeting; vibe_v5_hire / fire / add_researcher / remove_researcher; slash command /v5
All members	vibe_v5_say (group chat/direct message/to all voters), vibe_v5_wait (poll-free wait), vibe_v5_record_progress, vibe_v5_record_proposition / _method / _subproblem, vibe_v5_read_library (cross-read others' libraries, read-only), vibe_v5_propose_verify, vibe_v5_verdict, vibe_v5_task_create / _list / _get / _update, vibe_v5_meeting (propose)
Academician (also has the academicianLeads switch)	vibe_v5_overview (institute-wide overview), vibe_v5_assign (assignment, must state the reason and acceptance criteria), vibe_v5_prioritize, vibe_v5_nudge

Key Differences from v4

• There is a leader: v4 has no central scheduling and everything emerges from discussion; v5 has an academician responsible for organization and assignment inside the institute (the framework still never assigns —— the assigner is the academician, who is likewise bound by the m votes).
• The truth gate changes from "all-unanimous" to "≥ m unanimous" (switchable back to the v4 standard).
• State is stored in the session log's host-only projection cell, with DSH responsible for checkpoint/recovery (see above).
• Three classes of positions + hireable temp workers: the roster is mutable, and hiring/firing are real reversible operations.
• No npm experimental package is introduced: v5 is a single .js file within the preset, with zero dependencies.
• Meetings and verification are strictly mutually exclusive (queued in both directions).

See the v5 specification (written specification) and the v5 detail diagrams (all detail diagrams).

---

✨ Features

• Multi-agent automatic solving: the main agent hands the problem to the scheduler, which dispatches explorer / solver / verifier (v2/v3) plus subagents such as planner (planning agent, v3) and method-keeper (method organizing agent, v3) to solve collaboratively; you do not need to operate node by node by hand.
• Multi-agent cross-validation: every conclusion goes to ≥3 "strict reviewers" for independent review → debate (exchange group) → adjudication (v3 defaults to near-consensus adjudication: if on the same side and the mean is ≥0.85/≤0.15, take the mean, so that "0.9 vs 1" is not misjudged as 0.5).
• Paper-style Markdown knowledge base (v3): the problem list (including dependencies between problems, and the causes and plans of descendant problems), research log, propositions, and method library are all written and continued in md paper/research-report style (when a direction is re-derived, the logs of the old direction are automatically archived and kept); only Verified/ and the objects that a verifier judged true/false are absolutely trustworthy, and all other md (including unverified assertions in the method library) serve only as empirical reference.
• General theory invention library (v3): the theory systems/frameworks/tools/methods/ideas invented during solving (including empirical summaries) are reported via methods_used/new_inventions, and the Method Keeper consolidates them into Methods/ method cards (which can form a hierarchy of systems and be reused across projects), forming a systematic method–theory system just like "inventing group theory while solving equations".
• Planner-agent scheduling (v3): before scheduling, the planner agent is invoked to autonomously choose the optimal scheduling scheme according to the actual situation (problem dependencies / survival rate / verifiable objects / concurrency budget / results of the last plan), arranging the tasks of each agent for the next N steps in one go; if planning fails, it automatically falls back to heuristics.
• Knowledge accumulation: conclusions that pass verification are promoted into the Verified/ trustworthy knowledge base (v2/v3 additionally have the Propos/ proposition library) for reuse by later directions.
• Checkpoint resume: the scheduling state, task stack, agent registry, decision queue, verifier historical accuracy, etc. are all written to disk; after a restart, resume restores them (v2/v3 use a process epoch to distinguish "pause → resume within the same process" from "restart across processes"; v3's md is itself the narrative breakpoint).
• Mid-run manual intervention (and continue): the auto / manual modes can be switched at any time; in manual mode, a decision is suspended at key nodes and waits for your approve/reject/override (v3 adds a plan approval gate and a method promotion gate); you can send a message to / interrupt any subagent.
• Per-project isolation: each mathematical problem is an independent project folder, with no interference between them, and you can switch at any time.
• Multi-session parallel isolation: a DSH agent preset is a standing mount (all sessions of the same preset share one plugin instance), and inside the plugin all running state is isolated by root session id — two sessions can each run a project at the same time, their respective subagents are correctly attached under their own session, and the scheduler / parameters / decision queue / current project do not interfere with each other (v3 additionally has a project lock, so the same project is scheduled by only one session at a time). The current project is persisted per session (VibeMath/current.<session id>.json).
• Adjustable subagent permissions: you can restrict the tools a subagent is allowed/forbidden to use and the per-round cap on external tool calls, and explicitly tell it that it may read Verified/, Propos/, Methods/, Reliable/ and the progress log.
• Configurable: vibe_math_setting.json (with comments) for customizing default parameters; /vibe setup for interactive question-and-answer configuration.
• Natural-language control: the main agent acts as "assistant + reporter" — you state your needs in plain words, and it calls the tools, reports progress, and configures parameters on its own.

Specific to v4 / v5:

• Persistent self-organization (v4): at the start, N persistent resident subagents are created, after which all task arrangements are decided by those subagents themselves through leaving messages for each other + holding meetings (the framework only provides the message bus/meetings/task board, and never assigns tasks).
• Institute system (v5): on top of v4's self-organization, it introduces the organizational form of a real research institute — the academician (leader) is responsible for decomposition, assignment, prioritization, chairing meetings, and supervising progress; resident researchers have voting rights and can autonomously hire/fire their own temp workers; temp workers have no voting rights; all organizational actions are performed by members of the institute, and the framework still only acts as the medium. See the Vibe Math V5 section above for details.
• Adjustable quorum (v5): for an object to enter Verified/, ≥ m = min(quorumCap, number of enrolled voters) voters must cast a consistent boolean vote (all 1 or all 0); an opposing vote blocks, and abstentions do not count as votes but do count toward the average probability; if the threshold is not reached, the object is kept in the library with the average probability and the complete debate record, without forcing an adjudication.
• Zero-token-cost state persistence (v5): the institute state is stored in a host-only projection unit of the session log and does not enter the model context; cross-process and same-process recovery go through the same code path.
• Genuinely reversible roster (v5): hiring creates a resident child session; firing cancels in-flight turns, releases the child session, reclaims its tasks, and discards undelivered mail; a codename is never reused.
• Human-readable mirror (v4/v5): the roster table, task board, meeting minutes, debate records, and closing records are all written to disk as Markdown and are readable by humans at any time; but the authoritative state is not in these files (in v5 it is in the projection unit), so manually corrupting them will not break the institute.

---

🧮 Lean formal verification (shared by the four architectures, adjustable switch)

What it changes is not "being a bit stricter" but the object of review itself. m agents agreeing that "this is right" is still consensus — it cannot rule out shared misunderstanding; passing Lean is machine checking. The only remaining uncertainty is thus reduced to a question a single person can review effectively:

Are the definitions / objects / conditions / assumptions / conclusions in the Lean code fully consistent with the original text of the proposition?

	Original verification work	Verification work after formalization passes
Object of review	The proposition itself (whether the derivation is correct)	Fidelity: whether the Lean code ↔ the original text of the proposition are consistent
Strength of the conclusion	Consensus (may be jointly wrong)	Strict (already checked by the kernel), provided that fidelity holds
By-product	None	A reusable Lean definition / lemma library

Switch: formalVerify (same name in all four architectures, default 'off')

Value	Meaning
'off' (default)	No additional requirement whatsoever. No Lean content appears in member prompts, no formalization state is written, and the verification flow and gates are completely unchanged (it is a true no-op, guarded by assertions and probes). The three tools are still registered and usable (calling them proactively works as usual); the main agent's persona always lists these three tools and four parameters — otherwise the switch would not be discoverable, and "off" could not be turned on
'encourage'	Encouraged but not mandatory: at verification time, first judge the implementation difficulty of the object, and if it can be formalized within an acceptable amount of work, do that first; once Lean passes, the focus of review shifts to fidelity. In ordinary work, it is also encouraged to formalize and archive commonly used / potentially reusable objects, assumptions, and new definitions along the way. No gate
'require'	Mandatory: a true/false conclusion must satisfy "Lean has passed" or "the blocking reason has been explicitly recorded", otherwise this adjudication does not take effect — it is recorded as undecided (reason formal-required), written into the "formalization TODO", announced in the group chat, and the object is kept in the library to be re-proposed after formalization

"Explicitly record the blocking reason" in require is exactly where "decide not to do it based on implementation difficulty" lands: the decision is the agent's, but the decision must be spoken and auditable, and silently skipping is not allowed. Related parameters also include leanCommand (default lean), leanArgs (used with lake env lean), and leanTimeoutMs (default 120s).

⚠️ A fidelity defect ≠ the proposition is false (important)

Passing Lean only guarantees that "this piece of code passed the kernel"; it does not guarantee that it says what the proposition means to say. So when a voter, checking item by item, finds that the Lean code and the original text of the proposition are inconsistent (written too narrowly / too broadly / a different object / a missing condition):

• Do not vote 0. Voting 0 means "the proposition is false"; an incorrectly written formalization would make the framework record "the formalization does not qualify" as "the proposition was disproved", and under v5's all-0 consistency rule it would even write the proposition into Verified/ marked false — a mechanism meant for truth-seeking would instead fabricate a wrong negative conclusion.
• The correct approach: give a value strictly between 0 and 1 (recorded as an abstention) + use the receipt formal:{decision:'defect', note:'<specific deviation>'} to record the deviation. The framework then revokes the "passed" state of this proof (downgraded to attempted; Verified/Lean/<id>.lean is deleted, and if the host cannot delete it, it is rewritten as a "withdrawn" note, never leaving a withdrawn proof in the place where everyone looks for proofs; and it is written into the "formalization TODO"), and under the require setting this adjudication is not concluded (the encourage setting has no gate, so you must not claim that the framework will force a shelving — there it relies on voters abstaining to prevent a conclusion); vote again only after fixing the formalization and getting it to run through.
• Vote 0 only when the voter, independently of this Lean code, can also determine that the proposition is false (and can give independent reasons).

Receipt channel (members who do not call the Lean tools can also leave a judgment; it is mandatory under the require setting): "formal": {"target":"<object id>", "decision":"used|blocked|defect", "file":"Formal/<object id>.lean", "note":"difficulty judgment/blocking reason/specific deviation"}. When decision='blocked'/'defect', note is required (if missing, the whole entry is rejected); used only records the object as attempted; under the off setting this channel is disabled (otherwise off would not be a true no-op).

Three further hard requirements injected into the prompt (contract §6): tool names are always given in full (<prefix>lean_archive, not lean_archive — an abbreviation is not a registered name, and an agent copying it would call a nonexistent tool); before archiving a reusable definition/lemma, run it through first — if it does not run through, it must not enter the library; when the toolchain is missing (LEAN_NOT_FOUND cannot resolve the executable / NO_SUBPROCESS the host has no subprocess service), write the code down, archive it, and state "the host has no Lean toolchain" in note — this counts as an explicit blocking reason, and the gate lets it through on that basis, so it will not stall just because Lean cannot be installed.

Archive: where formalized code goes

<VibeMath root>/
├─ Formal/                              # ★ cross-project reusable library (shared by the four architectures)
│   ├─ Lib/<name>.lean                  # reusable definitions / objects / assumptions (def / structure / notation)
│   ├─ Lib/Index.md                     # name → file → category → summary (check here before writing a new definition)
│   ├─ Proved/<name>.lean               # established Lean propositions / lemmas (already machine-checked)
│   └─ Proved/Index.md
└─ Projects/<project>/                  # (in v5, Projects/<project>/Institutes/<institute>/)
    ├─ Formal/
    │   ├─ <object id>.lean              # formalization working file for this object
    │   ├─ Index.md                      # object → status → file → archived proof → run result → difficulty judgment
    │   └─ TODO.md                       # the "formalization TODO" under require mode
    └─ Verified/
        ├─ <original conclusion card>
        └─ Lean/<object id>.lean            # ★ archived proof: the formalized code corresponding to this conclusion object

Tools (three per architecture, prefix following each one's naming)

Tool	Purpose
<prefix>_lean_run	Execute Lean on the host subprocess service, returning {ok, exitCode, ms, stdout, stderr}. Never throws: missing toolchain → LEAN_NOT_FOUND, timeout → LEAN_TIMEOUT, path escape → rejected
<prefix>_lean_archive	kind='def'/'lemma' → archive to the cross-project Formal/Lib or Formal/Proved; kind='proof' → write Formal/<target>.lean, and if it runs through, also write Verified/Lean/<target>.lean and mark the object as Lean-passed; kind='blocked' → record an explicit difficulty judgment/blocking reason (reason required)
<prefix>_lean_lib	Rebuild and return the three indexes and the per-object formalization status — check for duplicates and reuse directly before writing a new definition

For example, v5 is vibe_v5_lean_run / vibe_v5_lean_archive / vibe_v5_lean_lib, v2/v3 are vibe_math_lean_*, and v4 is vibe_v4_lean_*.

Boundaries (intentional): the framework does not bundle Lean (it does not install a toolchain or download dependencies; when the toolchain is missing it degrades gracefully and records this faithfully); the framework does not judge fidelity (that is what agents/humans review and vote on; the framework is only responsible for switching the focus of review to fidelity); Lean passing ≠ the proposition is true — it only means "this piece of formalized code passed the kernel check".

For the complete contract (parameters, paths, state transitions, prompt semantics, gate locations, index format, test requirements), see docs/formal-verification.md.

The personas of all four presets (the prompt the main agent receives) fully list the three tools and four parameters above, and the two blocks prefix and text are identical line by line (only line 0 may differ). This layer is guarded by audit-persona-surface.test.mjs and audit-persona-sensitivity.mjs — when this feature was added, it was precisely in the four presets that the defect "the tools were registered but the persona never listed them" was found (the same batch also found that the persona listed two tools for adding/removing resident researchers too few, and that the /v4//v5 subcommand lists were inconsistent with the implementation; see the release notes shipped with the package).

---

🚀 Installation

Two installation methods, choose either one (they can also coexist):

Method A: one-click install as a plugin package (recommended, installs all four presets at once)

dsh plugin --profile <your profile> add dsh-vibe-math
# Or install directly from GitHub:
dsh plugin --profile <your profile> add github:ChongCyrus/Vibe-Mathematics

During installation the plugin automatically writes the four presets into ~/.dsh/.agent-presets/: vibe-math-v2/, vibe-math-v3/, vibe-math-v4/ and vibe-math-v5/. Then start a new session and pick Vibe Math V3 (v3, primary recommendation), Vibe Math V2 (v2, primary recommendation), Vibe Math V4 (v4, resident self-organization) or Vibe Math V5 (v5, institute system) in the preset picker — v2 and v3 are equally primary recommendations, choose according to your actual needs (see "How to choose"). After upgrading the package version, restart DSH; the managed files in these four preset directories will be replaced wholesale with the new version's bytes — including files you edited by hand. This is intentional: a preset that is "half old version, half new version" will fail to mount or behave strangely, and you cannot tell from the outside. The hand edits that get replaced are not lost: the original text is first backed up to ~/.dsh/.agent-presets/.vibe-math-backup/<old version>/<preset>/, and the file names are listed in the log (see the installer notes at the end for details). If you want to customize a preset, do not edit these managed files — make a copy (the copy action in the preset picker, or copy the directory yourself into a new id); that copy belongs to you and package updates will not touch it.

Method B: manual install as an agent preset

1. Copy the files from the corresponding directory of this repository into the preset directory:

   C:\Users\<you>\.dsh\.agent-presets\vibe-math-v2\   ← copy agent.cordis.yml / preset.yml / vibe-math-v2.js from vibe-math-v2/
   C:\Users\<you>\.dsh\.agent-presets\vibe-math-v3\   ← copy agent.cordis.yml / preset.yml / vibe-math-v3.js from vibe-math-v3/
   C:\Users\<you>\.dsh\.agent-presets\vibe-math-v4\   ← copy agent.cordis.yml / preset.yml / vibe-math-v4.js from vibe-math-v4/
   C:\Users\<you>\.dsh\.agent-presets\vibe-math-v5\   ← copy agent.cordis.yml / preset.yml / vibe-math-v5.js from vibe-math-v5/
   

2. Start a new session and select "Vibe Math V2" / "Vibe Math V3" / "Vibe Math V4" / "Vibe Math V5" in the preset picker.

3. Once the session starts it is ready to use: v2/v3 tools are vibe_math_*, v4 is vibe_v4_*, v5 is vibe_v5_*; typing /vibe, /v4, /v5 in the input box gives autocompletion.

After modifying preset files you must restart the DSH process before starting a new session (a preset's standing mount is cached until the process exits).

DSH version adaptation and dependencies

• Form dependencies: the four presets depend on DSH's standard agent-preset mechanism (~/.dsh/.agent-presets/<id>/ + preset picker) and bundle patch mechanism (cordis.patch.yml injects the installer).
• Host plugin rows: agent.cordis.yml references the @deepseek-ai/dsh-* plugin rows provided by the host (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, etc., about 21 unique package names). Missing rows on the host cause the preset mount to fail (an error is reported when the session starts).
• Host service APIs: the preset plugins consume subagents (startContinuable / sendMessage (continue/wake; followup is only a method of the Agent object, not a subagents service method) / interrupt / drainContinuableChildren (used by v5 for real dismissal)), agents (get/roots), tools (register/restrict), commands (register), fs (resolve/stat/readText/writeText/listDir), plus the optional subprocess / sandboxPolicy / compaction / sessionProjections / sessions. These API shapes evolve with DSH versions; this project has checked and adapted to them item by item on dsh-v0.1.5-rc.2 (dsh.testedVersion in package.json). Note: starting with DSH 0.1.2, subagents.startContinuable's agentOptions / toolFilter require the host provider to declare the corresponding capability (both the in-process spawn / fork providers support it; v4/v5's ability to specify member models/routes and tool permissions depends on this).

  2026 compatibility fix highlights (see docs/COMPAT-AUDIT-ROUND2.md for details): ① tools.restrict() throws on unregistered tool names, and the filter is applied when a subagent is created, so the permission name table must contain only names actually registered in this deployment — v2/v3 previously hard-coded web/fetch/bash (of which bash is disabled on Windows), which caused "when you want to tighten permissions, the subagent can never start"; ② v4's real /compact previously looked up agents.get() in subagent/end, but that event fires only after the subagent has already been removed from the registry, making it dead code; it now captures the reference in subagent/start; ③ optional services are now read lazily instead of being snapshotted in apply() (otherwise mount order could leave subprocess permanently undefined and silently skip directory creation).

• DSH STORE compatibility declaration: dsh.compatibility.dshReleases in package.json declares compatible / incompatible / unknown item by item for each complete DSH version (currently 8 versions from 0.1.2-alpha.4 … 0.1.5-rc.2 are declared compatible, with 0.1.5-rc.2 as the tested target); engines.node is ^22.19.0 || >=24.0.0.
• Runtime self-check (capability + version dual check): on every start the installer (bundle plugin): ① makes a best-effort probe of the DSH version (reads @deepseek-ai/dsh/package.json or the DSH_VERSION environment variable; DSH does not expose its version through a public service/context, so this is best effort and is skipped if the probe fails). If a version is detected and is not declared compatible in dshReleases, a clear notice is given; ② then runs a capability self-check against host services and key APIs (this is the real mount gate): subagents/agents/tools/commands/fs are required (missing means a warning), while subprocess/sandboxPolicy/compaction/sessionProjections/sessions are optional (missing only prompts that "functionality will silently degrade" and does not affect mounting; when sessionProjections is missing, v5's institute state falls back to hardened JSON), and it also includes an fs.resolve return-shape check and a subagent agentOptions/toolFilter capability check. If a preset fails to mount, look first at the self-check warnings in the DSH log.
• Upgrade path: after upgrading DSH there is no need to reinstall this package; to upgrade this package use dsh plugin --profile <your profile> add dsh-vibe-math@latest (dsh plugin's --profile is mandatory; use add rather than update, because a profile may pin the version to an exact value, in which case update will not cross over), and after restarting DSH the installer updates the managed files of the four presets wholly to the new version (modified files are likewise replaced, with the original text first going to <presetRoot>/.vibe-math-backup/; see the "Installation" notes above).

---

🧭 How to choose among the four presets

💡 vibe-math-v2 and vibe-math-v3 are equally primary recommendations; choose according to your actual needs:

• Choose vibe-math-v2 (probability-driven · JSON data layer) if you:
  • prefer structured JSON data (qs.json / Propos/<category>_Propos.json / Verified/ cards), convenient for programmatic retrieval and further processing;
  • want mature and stable code-heuristic scheduling (priority + probability, predictable behavior, not dependent on the planner agent's "improvisation");
  • do not need method library accumulation / paper-style narration, and data bei

…