|
3 | 3 | from __future__ import annotations |
4 | 4 |
|
5 | 5 | SERVER_DESCRIPTION = ( |
6 | | - "Use atomic exact and symbolic mathematics, with separate checker operations " |
7 | | - "when independent verification is needed." |
| 6 | + "Search and run installed Jacobian exact-math operations, with separate checker " |
| 7 | + "operations for independent verification." |
8 | 8 | ) |
9 | 9 |
|
10 | 10 | SERVER_INSTRUCTIONS = ( |
11 | | - "Use Jacobian whenever a task may benefit from a specialized exact mathematical " |
12 | | - "operation, including matrix or polynomial computation. This applies even when the " |
13 | | - "user does not name Jacobian and shell code could also calculate the result. Unless " |
| 11 | + "Search and run the locally installed Jacobian toolbox whenever a task may benefit " |
| 12 | + "from exact computation, symbolic transformation, finite search, formal inspection, " |
| 13 | + "or independent checking, even when the user does not name Jacobian or shell code " |
| 14 | + "could also calculate the result. math.find is the authoritative local inventory; " |
| 15 | + "internet search cannot show which operations are available in this runtime. Unless " |
14 | 16 | "an exact installed capability ID and its typed contract are already available, call " |
15 | | - "math.find with a plain-language desired local mathematical outcome; no capability " |
16 | | - "ID is required. math.run may execute a known contract directly. " |
| 17 | + "math.find with a plain-language desired local mathematical outcome. math.run may " |
| 18 | + "execute a known contract directly. " |
17 | 19 | "For declaration queries explicitly targeting Jacobian's pinned CORE or MATHLIB " |
18 | 20 | "environment, use the pinned mathematical operation; do not substitute repository " |
19 | 21 | "search, cached Mathlib files, or a local Lean process because they may not match " |
20 | | - "that server environment. Project-local Lean " |
21 | | - "declarations are outside the server catalog and may require project-local tools. " |
22 | | - "Other uses include symbolic transformation, structural analysis, examples or " |
23 | | - "counterexamples, bounded search, Lean/Mathlib declaration search or formal-" |
24 | | - "environment inspection, and requested independent verification. " |
25 | | - "Do not report that no specialized mathematical operation is available without " |
26 | | - "checking math.find. When independent checking is requested, multiple calculations " |
27 | | - "or programs authored by the same model are not independent checker evidence. " |
28 | | - "Search again whenever the objective or available evidence changes. " |
| 22 | + "that server environment. Project-local Lean declarations are outside the server " |
| 23 | + "catalog and may require project-local tools. Repeating the same lookup against an " |
| 24 | + "unchanged catalog returns the same operation facts; math.find is operation lookup, " |
| 25 | + "not confirmation. Merely restating an accepted value without new evidence is not a " |
| 26 | + "mathematical-tool use case. " |
29 | 27 | "The model owns representation, decomposition, composition, iteration, verification " |
30 | | - "timing, and stopping. Results keep execution status, mathematical conclusion, " |
31 | | - "and verification record separate. No descriptor match, timeout, " |
32 | | - "bounded or exhausted search, or failure to find a witness is a mathematical " |
33 | | - "conclusion. Only a result with a local verification record URI is " |
34 | | - "verified. A verification record for an input, premise, factorization, or related " |
35 | | - "artifact does not verify a model-derived conclusion; the record must be bound to " |
36 | | - "the exact final claim." |
| 28 | + "timing, and stopping. An operation match, timeout, incomplete search, or failure to " |
| 29 | + "find a witness is not a mathematical conclusion. Independent checking uses a " |
| 30 | + "separate checker operation; model-authored duplicate calculations are not independent " |
| 31 | + "evidence. Only a result with a local verification record URI is verified. A record " |
| 32 | + "for an input, premise, factorization, or related artifact does not verify a model-" |
| 33 | + "derived conclusion; the record must be bound to the exact final claim." |
37 | 34 | ) |
38 | 35 |
|
39 | 36 | MATH_FIND_DESCRIPTION = """\ |
40 | | -Search or inspect installed math tools by desired outcome or exact ID. Use when a |
41 | | -task may benefit from exact computation, search, structural analysis, or a separate |
42 | | -checker tool—even if shell code could also calculate the answer. |
| 37 | +Search or inspect locally installed Jacobian math tools by desired outcome or exact ID. |
| 38 | +This is the authoritative runtime inventory; internet search is not. Use when a task |
| 39 | +may benefit from exact computation, search, structural analysis, or a separate checker |
| 40 | +tool—even if shell code could also calculate the answer. |
43 | 41 |
|
44 | 42 | Forms: |
45 | 43 | - `request.op="search"`: plain-language mathematical outcome (compact cards). |
|
58 | 56 | """ |
59 | 57 |
|
60 | 58 | MATH_RUN_DESCRIPTION = """\ |
61 | | -Run one installed math tool by ID with its typed `payload`. Read the mathematical |
62 | | -value in `output` first, then execution status. If the payload shape is unknown, |
63 | | -inspect the exact operation with math.find, then copy and adapt one of its |
64 | | -`invocation_examples`. Do not call math.run with an empty `payload` merely to |
65 | | -discover required fields; the inspect result is the authoritative contract. |
| 59 | +Run one installed math tool by ID with its typed `payload`. Check execution status |
| 60 | +before treating `output` as mathematical evidence. For a completed run, interpret the |
| 61 | +operation-owned result fields and any `verification_record_uri` to determine exactly |
| 62 | +what the run established. If the payload shape is unknown, inspect the exact operation |
| 63 | +with math.find and copy its `invocation_examples`. Do not call math.run with an empty |
| 64 | +`payload` merely to discover required fields; the inspect result is the authoritative |
| 65 | +contract. |
66 | 66 |
|
67 | 67 | Ordinary tools return calculations. Independent checking uses a separate checker |
68 | 68 | tool ID (for example `polynomial.identity.verify`), not a switch on the producer. |
69 | | -Failed or incomplete runs are not mathematical conclusions. |
| 69 | +Failed, cancelled, timed-out, or incomplete runs are not mathematical conclusions. |
70 | 70 |
|
71 | 71 | Examples: |
72 | 72 | - `{"capability_id":"integer.compute.gcd","payload":{"left":"84","right":"30"}}` |
|
0 commit comments