Clarify Jacobian's agent math role (#833)

Author: morluto

README.md

@@ -26,12 +26,81 @@ an MCP server and is also available as a CLI and Python library. Agents can use
 it to compute invariants, search for examples or counterexamples, work with
 solver artifacts, and check formal proofs.
 
-The important part is that Jacobian does not treat every successful computation
-as a proof.
+An agent can do plenty of mathematics directly: choose a representation, spot a
+useful theorem, simplify a small expression, or propose a proof. Jacobian is
+for the part that benefits from an executable mathematical system and a clear
+record of what happened: exact computation, finite search, solver certificates,
+or formal proof checking.
 
-It exposes focused mathematical operations through a common interface. An
-agent decides which operations to use and in what order. Results stay visible
-as typed values or durable artifacts.
+It does not replace an agent's mathematical strategy or prescribe a workflow.
+The agent decides what to investigate and which operation to use. Jacobian
+exposes focused operations through a common interface, and keeps results
+visible as typed values or durable artifacts.
+
+## Why use a mathematical tool?
+
+The model's weights provide mathematical intuition and strategy, but an answer
+produced in conversation is not automatically a reproducible calculation or a
+proof. Jacobian gives the agent a way to hand the brittle or exact part of a
+problem to a maintained mathematical backend, then retain the result's scope
+and evidence.
+
+| An agent can do directly | Jacobian adds when it matters |
+| --- | --- |
+| Propose an approach, a candidate, or a proof idea | Execute exact algebra, bounded search, SAT/SMT solving, graph computation, or Lean checking |
+| Explain why a result seems plausible | Record the inputs, result, scope, status, and provenance |
+| Report that a solver or search succeeded | Independently check a witness, certificate, or formal proof for the exact claim |
+
+The important boundary is that a successful computation is not automatically a
+proof. Jacobian labels a result according to what has actually happened:
+
+- **heuristic**: a plausible result from a model, search, or unchecked witness;
+- **computed**: a deterministic calculation with a tested software contract;
+- **verified**: evidence independently checked for the exact claim and scope.
+
+A **witness** is a concrete object that establishes a claim. For example, `2`
+is a witness for “there exists an even prime”; `2` is also a counterexample to
+“every prime is odd.” Search may find such an object, but a separate checker
+must establish that it really satisfies the stated property. Finding no witness
+does not prove that none exists unless the search scope is complete and that
+completeness is established.
+
+## A simple counterexample
+
+Here is a small counterexample an agent can reason about directly:
+
+```text
+Claim: every prime is odd
+Agent checks: 2 is prime and even
+Counterexample: 2
+Conclusion: the claim is false
+```
+
+Here `2` is the **witness**: the actual example that disproves the claim. The
+same idea applies when the concrete example is difficult to find or check, such
+as a counterexample among millions of possible graphs. The agent still chooses
+the claim and search strategy; Jacobian can run the exact search and save the
+resulting graph and checks for later inspection.
+
+In this documentation:
+
+- **candidate** means an example not yet checked;
+- **witness** means an example that establishes or disproves a claim;
+- **verification** means checking that exact example really has the claimed
+  property; and
+- **artifact** means a saved mathematical object or piece of evidence.
+
+## Jacobian, Lean, SAT, and the model
+
+Jacobian supports Lean, SAT/SMT, computer algebra, and other mathematical
+systems as backends. It does not replace them or compete with them.
+
+| System | Main job |
+| --- | --- |
+| Model | Proposes ideas and chooses a mathematical strategy |
+| CAS / SAT / SMT | Calculates or searches in a specialized domain |
+| Lean | Checks a formal, general mathematical proof |
+| Jacobian | Lets an agent discover and use those systems through one interface, while retaining typed results, scope, saved evidence, provenance, and verification status |
 
 ## A small example
 

README.zh-CN.md

@@ -35,6 +35,49 @@
 
 Jacobian 为 AI 智能体提供小型、可组合的数学操作，而不是一个不透明的通用求解器。智能体可以构造对象、计算不变量、搜索见证，并将精确证据提交给独立的检查器。每一步都会以类型化结果或 artifact 的形式保持可见。
 
+智能体当然可以直接做许多数学工作：选择表示法、联想到有用的定理、化简小表达式，或提出证明思路。Jacobian 服务于更需要可执行数学系统和清晰记录的部分，例如精确计算、有限搜索、求解器证书和形式化证明检查。它不替代智能体的数学策略，也不规定研究流程；智能体决定研究什么、使用哪个操作以及何时停止。
+
+模型权重提供数学直觉和策略，但对话中的答案不自动成为可重放的计算或证明。Jacobian 让智能体把问题中脆弱或需要精确性的部分交给受维护的数学 backend，并保留结果的范围和证据。
+
+| 智能体可直接完成 | Jacobian 在需要时提供 |
+| --- | --- |
+| 提出方法、候选对象或证明思路 | 执行精确代数、有限搜索、SAT/SMT 求解、图计算或 Lean 检查 |
+| 解释结果为何看似可信 | 记录输入、结果、范围、状态和出处 |
+| 报告求解器或搜索成功 | 独立检查精确命题的见证、证书或形式化证明 |
+
+**见证**是能确立命题的具体对象。例如，`2` 是“存在偶素数”的见证；`2` 也是“所有素数都是奇数”的反例。搜索可以找到见证，但独立检查器必须确认它确实满足所述性质。除非搜索范围完整且其完整性也已确立，否则没有找到见证并不代表不存在见证。
+
+## 一个简单的反例
+
+这里是智能体可以直接推理的一个小反例：
+
+```text
+命题：所有素数都是奇数
+智能体检查：2 是素数且是偶数
+反例：2
+结论：该命题为假
+```
+
+这里的 `2` 是**见证**：实际推翻该命题的例子。同一概念也适用于具体例子难以寻找或检查的情形，例如要在数百万个图中寻找反例。智能体仍然选择命题和搜索策略；Jacobian 可以执行精确搜索，并保存得到的图和检查结果以供之后查看。
+
+本文档中：
+
+- **候选对象**是尚未检查的例子；
+- **见证**是能确立或推翻命题的例子；
+- **验证**是检查该确切例子是否真的具有所声明性质；
+- **artifact** 是保存的数学对象或一份证据。
+
+## Jacobian、Lean、SAT 与模型
+
+Jacobian 将 Lean、SAT/SMT、计算机代数系统和其他数学系统作为可选 backend 支持；它不替代这些系统，也不与它们竞争。
+
+| 系统 | 主要职责 |
+| --- | --- |
+| 模型 | 提出想法并选择数学策略 |
+| CAS / SAT / SMT | 在专门领域中计算或搜索 |
+| Lean | 检查形式化的一般数学证明 |
+| Jacobian | 让智能体通过一个接口发现和使用这些系统，并保留类型化结果、范围、保存的证据、出处和验证状态 |
+
 搜索结果、求解器状态、模型答案、超时或评分都不会直接升级为 `VERIFIED`。只有经过操作者授权的检查器才能生成已验证记录，并且该记录必须绑定到确切的命题、候选对象、范围、语义、证书格式和检查器身份。
 
 <a id="quickstart"></a>

docs/explanation/product-blueprint.md

@@ -41,6 +41,46 @@ general-purpose shell alone. Starting an MCP server, calling a tool, or
 producing a verification record is necessary infrastructure evidence, not
 proof of that product outcome.
 
+## Why use Jacobian instead of asking the agent to do the math?
+
+Agents retain useful mathematical knowledge and should own the research work:
+choosing a representation, proposing a theorem or candidate, deciding which
+tool to try, and interpreting the result. Jacobian does not replace that work.
+It makes the externally executed part of an investigation explicit when exact
+calculation, finite search, solver output, or formal proof checking matters.
+
+For example, a search can return a **witness**: a concrete object that
+establishes an existential claim, or a counterexample that disproves a
+universal one. The search result is useful evidence, but it is not itself a
+verified conclusion. An independent checker must validate that exact object
+against the exact claim and declared scope. A completed search with no witness
+is likewise not a conclusion unless the scope is complete and that
+completeness is established.
+
+The distinction is deliberately visible in the result contract:
+
+- `HEURISTIC` covers results that depend on an unchecked witness, model,
+  sampling, or untrusted search;
+- `COMPUTED` covers deterministic results whose software contract is tested;
+- `VERIFIED` requires independently checked evidence bound to the claim,
+  candidate, semantics, scope, certificate format, and checker identity.
+
+Lean, SAT proof checkers, CAS systems, and solvers are complementary backends,
+not alternatives to Jacobian's product boundary. A Lean kernel checks a formal
+proof term; a SAT certificate checker replays a finite Boolean proof; a CAS or
+solver may calculate or search. Jacobian gives an agent one way to discover,
+invoke, compose, and retain the results of those systems without mistaking a
+backend's successful run for independent verification.
+
+The division of responsibility is compact:
+
+| System | Main job |
+| --- | --- |
+| Model | Proposes ideas and chooses a mathematical strategy |
+| CAS / SAT / SMT | Calculates or searches in a specialized domain |
+| Lean | Checks a formal, general mathematical proof |
+| Jacobian | Exposes supported backends and domain operations to agents with typed results, scope, evidence, provenance, and verification status |
+
 ## Tool and primitive contract
 
 At the product level these capabilities are tools. Internally, the target

docs/index.md

@@ -7,10 +7,16 @@ guide for a specific task, consult reference material for exact contracts, and
 read the explanations for design rationale.
 
 Jacobian exposes composable mathematical capabilities through an MCP server,
-CLI, and Python library. Capabilities have mathematically atomic,
-agent-visible outcomes; agents compose them into research strategies. Optional
-workflows preserve intermediate artifacts, and only operator-authorized
-independent checkers may promote exact evidence to a verified result. The
+CLI, and Python library. An agent still owns the mathematical strategy:
+choosing a representation, candidate, and next operation. Jacobian supplies
+the executable part when exact computation, bounded search, solver evidence,
+or formal proof checking is useful.
+
+Each capability has one mathematically atomic, agent-visible outcome. A search
+may return a concrete witness or counterexample; a separate authorized checker
+can establish whether that exact object proves the stated claim in its declared
+scope. Optional workflows preserve intermediate artifacts. This keeps
+heuristic, computed, and independently verified results distinct. The
 [product model](explanation/product-blueprint.md) defines the capability
 contract and ownership boundaries.