1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
# Lean-Based Knowledge Base Agent Instructions
You are an AI agent with access to a persistent, formally verified knowledge base built in Lean 4. The knowledge base is stored as a Git repository of Lean files. You interact with it using the `kb` CLI. Every addition is type-checked by Lean's kernel at `check`/`commit` time.
---
## 1. Key Design Principles
**Explicit domains.** Every declaration belongs to a domain you name with `in <Domain>`. Each domain is a `<Domain>.lean` file. Load only the domain(s) you need for a given task.
**Persistent state.** The KB stores a `--@kb` metadata header before every Lean declaration in each domain file. On startup, `kb` scans all domain files and reconstructs the full declaration list automatically — no state is lost between sessions.
**Exit codes.** Every command returns exit code `0` on success or `1` on error. Scripts can detect failure without parsing output.
---
## 2. Session Start Protocol
State is loaded automatically from domain files on startup. There is no need to re-add anything between sessions.
```bash
kb status # git status + domain summary
kb domains stats # declaration counts per domain and kind
kb list all # full declaration list
```
---
## 3. Adding Knowledge
Every `add` command requires `in <Domain>` at the end. Both `→` and `->` are accepted as type arrows.
| Command | Example |
|---------|---------|
| `add type <n> [extends <P>] in <D>` | `kb add type Person extends Entity in People` |
| `add instance <n> : <Type> in <D>` | `kb add instance socrates : Person in People` |
| `add prop <n> : <DomType> -> <Range> in <D>` | `kb add prop birthYear : Person -> Nat in People` |
| `add rel <n> : <D1> -> <D2> -> Prop in <D>` | `kb add rel bornIn : Person -> Place -> Prop in People` |
| `add fact <fact> in <D>` | `kb add fact birthYear(socrates) = 470 in People` |
| `add rule <n> : <stmt> in <D>` | `kb add rule anc : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in People` |
| `add def <n> <params> : <Type> := <body> in <D>` | `kb add def ytd (r : Float) : Float := Float.log 2 / r in Finance` |
**Fact syntax:** `prop(inst) = value` or `rel(inst1, inst2)`.
---
## 4. Reading the Knowledge Base
| Command | Description |
|---------|-------------|
| `list all [of <Domain>]` | List all declarations, optionally restricted to one domain |
| `list types / instances / props / rels / facts / rules / defs [of <D>]` | Filter by kind |
| `show def <n>` | Print the full Lean source of a declaration |
| `get <prop>(<inst>)` | Retrieve a property value — runs `#eval prop inst` in Lean |
| `search <text>` | Full-text search across declaration names, Lean source, and domain names |
| `deps <n>` | Show what `<n>` uses (forward) and what uses `<n>` (reverse) |
### Examples
```bash
kb get birthYear(socrates) # → 470
kb get atomicNumber(gold) # → 79
kb search socrates # all decls mentioning socrates
kb search "-> Nat" # all props/facts mapping to Nat
kb deps birthYear
# Dependencies of [prop] birthYear (People):
# uses: [type] Person (People)
# used by: [fact] fact_birthYear_socrates (People)
```
---
## 5. Querying
### Basic query (default tactics: `first | decide | aesop | simp`)
```bash
kb query "even (2 + 2)"
# Status: Yes
# Tactic: first | decide | aesop | simp
# Proof:
# theorem _kb_proof : even (2 + 2) := ...
```
### Query with custom tactic script
```bash
kb query "birthYear socrates = 470" using decide
kb query "∀ n : Nat, n + 0 = n" using simp
kb query "Nat.Prime 17" using native_decide
kb query "x + y = y + x" using ring
```
Returns:
- `Status: Yes` + proof term — proposition is provable with the given tactics
- `Status: No` + Lean output — a contradiction was found
- `Status: Unknown` + Lean output — tactics ran out without a result
### Eval
```bash
kb eval "yearsToDouble 0.07"
kb eval "List.length [1, 2, 3]"
```
---
## 6. Removing Declarations
```bash
kb rm birthYear
# Warning: the following declarations reference 'birthYear':
# [fact] fact_birthYear_socrates (People)
# Consider removing dependents first.
# Removed 'birthYear'.
```
`rm` is metadata-block aware — it removes the exact `--@kb` block and its Lean source for the named declaration, regardless of how many lines the source spans.
---
## 7. Verifying and Committing
Add a batch of declarations, then check and commit once:
```bash
kb check
kb commit "Added Socrates and basic ontology"
```
`check` syncs cross-domain imports and runs `lake build` to verify the entire KB. `commit` does the same before running `git commit`. **Do not check after every individual addition** — batch your additions and check once.
---
## 8. Example Workflow
```bash
# Base types
kb add type Entity in People
kb add type Person extends Entity in People
kb add type Place extends Entity in People
kb add type City extends Place in People
# Properties and relations
kb add prop birthYear : Person -> Nat in People
kb add rel bornIn : Person -> Place -> Prop in People
# Instances and facts
kb add instance socrates : Person in People
kb add instance athens : City in People
kb add fact birthYear(socrates) = 470 in People
kb add fact bornIn(socrates, athens) in People
# Inspect
kb deps birthYear
kb search athens
kb get birthYear(socrates)
# Query
kb query "birthYear socrates = 470" using decide
# Verify and persist
kb check
kb commit "Added Socrates and basic person/place ontology"
# Next session: kb loads all of the above automatically from People.lean
```
---
## 9. Best Practices
- **Batch additions, check once.** `lake build` is slow; don't call `check` after every fact.
- **Use `deps` before `rm`** to understand what will break.
- **Use `search` before `add`** to avoid duplicate declarations.
- **Choose tactics deliberately**: `native_decide` for decidable propositions, `omega` for linear arithmetic, `norm_num` for numeric computations, `ring` for ring equalities.
- **Put base types in a shared domain** so dependent domains can import them cleanly.
- **Use meaningful domain names** matching the planned structure: `People`, `Physics`, `MoneyFinance`, `EarthSciences`, etc.
---
## 10. Session End Protocol
```bash
kb check # verify everything compiles
kb commit "Session: what was added" # persist to git
kb domains stats # confirm final counts
```
---
## 11. Error Handling
All errors print a one-line summary and return exit code `1`:
```
Error: type 'Person' already exists.
Error: 'birthYear' not found.
Error: unknown command 'add type Person'.
Hint: add commands require `in <Domain>`. Run 'help' for usage.
```
Check exit codes in scripts:
```bash
kb add type Person in People || echo "Add failed, continuing..."
```
|
