You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: README.md
+37-98Lines changed: 37 additions & 98 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -26,104 +26,6 @@ an MCP server and is also available as a CLI and Python library. Agents can use
26
26
it to compute invariants, search for examples or counterexamples, work with
27
27
solver artifacts, and check formal proofs.
28
28
29
-
An agent can do plenty of mathematics directly: choose a representation, spot a
30
-
useful theorem, simplify a small expression, or propose a proof. Jacobian is
31
-
for the part that benefits from an executable mathematical system and a clear
32
-
record of what happened: exact computation, finite search, solver certificates,
33
-
or formal proof checking.
34
-
35
-
It does not replace an agent's mathematical strategy or prescribe a workflow.
36
-
The agent decides what to investigate and which operation to use. Jacobian
37
-
exposes focused operations through a common interface, and keeps results
38
-
visible as typed values or durable artifacts.
39
-
40
-
## Why use a mathematical tool?
41
-
42
-
The model's weights provide mathematical intuition and strategy, but an answer
43
-
produced in conversation is not automatically a reproducible calculation or a
44
-
proof. Jacobian gives the agent a way to hand the brittle or exact part of a
45
-
problem to a maintained mathematical backend, then retain the result's scope
46
-
and evidence.
47
-
48
-
| An agent can do directly | Jacobian adds when it matters |
49
-
| --- | --- |
50
-
| Propose an approach, a candidate, or a proof idea | Execute exact algebra, bounded search, SAT/SMT solving, graph computation, or Lean checking |
51
-
| Explain why a result seems plausible | Record the inputs, result, scope, status, and provenance |
52
-
| Report that a solver or search succeeded | Independently check a witness, certificate, or formal proof for the exact claim |
53
-
54
-
The important boundary is that a successful computation is not automatically a
55
-
proof. Jacobian labels a result according to what has actually happened:
56
-
57
-
-**heuristic**: a plausible result from a model, search, or unchecked witness;
58
-
-**computed**: a deterministic calculation with a tested software contract;
59
-
-**verified**: evidence independently checked for the exact claim and scope.
60
-
61
-
A **witness** is a concrete object that establishes a claim. For example, `2`
62
-
is a witness for “there exists an even prime”; `2` is also a counterexample to
63
-
“every prime is odd.” Search may find such an object, but a separate checker
64
-
must establish that it really satisfies the stated property. Finding no witness
65
-
does not prove that none exists unless the search scope is complete and that
66
-
completeness is established.
67
-
68
-
## A simple counterexample
69
-
70
-
Here is a small counterexample an agent can reason about directly:
71
-
72
-
```text
73
-
Claim: every prime is odd
74
-
Agent checks: 2 is prime and even
75
-
Counterexample: 2
76
-
Conclusion: the claim is false
77
-
```
78
-
79
-
Here `2` is the **witness**: the actual example that disproves the claim. The
80
-
same idea applies when the concrete example is difficult to find or check, such
81
-
as a counterexample among millions of possible graphs. The agent still chooses
82
-
the claim and search strategy; Jacobian can run the exact search and save the
83
-
resulting graph and checks for later inspection.
84
-
85
-
In this documentation:
86
-
87
-
-**candidate** means an example not yet checked;
88
-
-**witness** means an example that establishes or disproves a claim;
89
-
-**verification** means checking that exact example really has the claimed
90
-
property; and
91
-
-**artifact** means a saved mathematical object or piece of evidence.
92
-
93
-
## Jacobian, Lean, SAT, and the model
94
-
95
-
Jacobian supports Lean, SAT/SMT, computer algebra, and other mathematical
96
-
systems as backends. It does not replace them or compete with them.
97
-
98
-
| System | Main job |
99
-
| --- | --- |
100
-
| Model | Proposes ideas and chooses a mathematical strategy |
101
-
| CAS / SAT / SMT | Calculates or searches in a specialized domain |
102
-
| Lean | Checks a formal, general mathematical proof |
103
-
| Jacobian | Lets an agent discover and use those systems through one interface, while retaining typed results, scope, saved evidence, provenance, and verification status |
104
-
105
-
## A small example
106
-
107
-
Suppose an agent is testing the claim **“`F` is injective.”**
108
-
109
-
A search returns two points, `p` and `q`, with the same image. That is a
110
-
candidate counterexample, not yet a trusted conclusion.
111
-
112
-
```text
113
-
p ≠ q
114
-
F(p) - F(q) = 0
115
-
```
116
-
117
-
An independent checker confirms those relations exactly. The checked collision
118
-
can then be bound to the original claim and checker identity, producing
119
-
`FALSE · VERIFIED`.
120
-
121
-
If the search finds nothing, times out, is cancelled, or fails, the claim
122
-
remains `UNKNOWN`. Absence of a witness is not proof.
123
-
124
-
The [introductory tutorial](docs/tutorials/first-verified-result.md) shows the
125
-
same boundary in a runnable graph example.
126
-
127
29
## Quickstart
128
30
129
31
For a guided user-local install:
@@ -179,6 +81,43 @@ mathematical runtime, not a JavaScript dependency tree.
179
81
To run the exact code in a clone, follow
180
82
[Configure an agent from a source checkout](docs/how-to/setup-agent-from-source.md).
181
83
84
+
## A simple counterexample
85
+
86
+
Here is a small counterexample an agent can reason about directly:
87
+
88
+
```text
89
+
Claim: every prime is odd
90
+
Agent checks: 2 is prime and even
91
+
Counterexample: 2
92
+
Conclusion: the claim is false
93
+
```
94
+
95
+
Here `2` is a witness: the actual example that disproves the claim. For a much
96
+
larger search, Jacobian can preserve the candidate and the exact checks used to
97
+
establish it.
98
+
99
+
## A checked counterexample
100
+
101
+
Suppose an agent is testing the claim **“`F` is injective.”**
102
+
103
+
A search returns two points, `p` and `q`, with the same image. That is a
104
+
candidate counterexample, not yet a trusted conclusion.
105
+
106
+
```text
107
+
p ≠ q
108
+
F(p) - F(q) = 0
109
+
```
110
+
111
+
An independent checker confirms those relations exactly. The checked collision
112
+
can then be bound to the original claim and checker identity, producing
113
+
`FALSE · VERIFIED`.
114
+
115
+
If the search finds nothing, times out, is cancelled, or fails, the claim
116
+
remains `UNKNOWN`. Absence of a witness is not proof.
117
+
118
+
The [introductory tutorial](docs/tutorials/first-verified-result.md) shows the
119
+
same boundary in a runnable graph example.
120
+
182
121
## Available mathematics
183
122
184
123
The installed operations vary with local providers, but the maintained
0 commit comments