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
|
# 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` command-line tool. Every addition is type-checked by Lean's kernel, ensuring logical consistency.
---
## 1. Key Design Principle: Explicit Domains
Every declaration belongs to a **domain** that you name explicitly using `in <Domain>`. Each domain is stored as a separate `<Domain>.lean` file in the KB root. There is no automatic classification.
**Choose domains based on what you want an agent to load together.** For example:
- `Ontology` — base types (`Entity`, `Person`, `Place`, …) that everything else depends on
- `People` — instances, properties, and facts about specific people
- `Geography` — instances and facts about places
- `Finance` — financial formulas and data
- `Physics` — physical constants and laws
An agent loading only `People` facts into its context window would run: `kb list all of People`.
---
## 2. Session Start Protocol
```bash
# Orient yourself: see what domains and declarations exist
kb list all
kb domains stats
# Recall declarations in a specific domain
kb list all of Ontology
kb list all of People
```
---
## 3. Adding Knowledge
Every `add` command requires `in <Domain>` at the end.
| Command | Purpose | Example |
|---------|---------|---------|
| `kb add type <n> [extends <Parent>] in <D>` | Declare a type | `kb add type Person extends Entity in Ontology` |
| `kb add instance <n> : <Type> in <D>` | Declare an individual | `kb add instance socrates : Person in People` |
| `kb add prop <n> : <DomType> -> <Range> in <D>` | Declare a property | `kb add prop birthYear : Person -> Nat in People` |
| `kb add rel <n> : <D1> -> <D2> -> Prop in <D>` | Declare a relation | `kb add rel bornIn : Person -> Place -> Prop in People` |
| `kb add fact <fact> in <D>` | Assert a fact | `kb add fact birthYear(socrates) = 470 in People` |
| `kb add rule <n> : <statement> in <D>` | Add a logical rule | `kb add rule ancestors_transitive : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in Ontology` |
| `kb add def <n> <params> : <Type> := <body> in <D>` | Define a shortcut | `kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance` |
### Notes
- Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows.
- Fact syntax: `prop(inst) = value` or `rel(inst1, inst2)`.
- Domains are created automatically when first used — no `create domain` step needed.
- Put base types in a shared domain (e.g. `Ontology`) that other domains can depend on.
---
## 4. Querying the Knowledge Base
| Command | Description | Example |
|---------|-------------|---------|
| `kb eval <expr>` | Compute a value | `kb eval "yearsToDouble 0.05"` |
| `kb query <prop>` | Ask if a proposition is provable | `kb query "even (2 + 2)"` |
| `kb list all of <Domain>` | List all declarations in a domain | `kb list all of People` |
### Query semantics
- `kb eval` runs Lean's `#eval` on the expression.
- `kb query` attempts to prove the proposition using `decide`, `aesop`, or `simp`. Returns `Yes`, `No`, or `Unknown`.
---
## 5. Checking Consistency and Committing
Add all facts first, then verify and commit in one step:
```bash
kb check
kb commit "Added Socrates and basic ontology"
```
`kb check` rewrites `KnowledgeBase.lean` to import every domain file on disk, injects cross-domain imports where needed, then runs `lake build`. `kb commit` does the same before committing to Git.
**Do not check after each individual fact.** Batch your additions, then check once.
---
## 6. Example Workflow
```bash
# Base ontology (shared types everything else depends on)
kb add type Entity in Ontology
kb add type Person extends Entity in Ontology
kb add type Place extends Entity in Ontology
kb add type City extends Place in Ontology
# Domain-specific properties and relations
kb add prop birthYear : Person -> Nat in People
kb add rel bornIn : Person -> Place -> Prop in People
# Instances
kb add instance socrates : Person in People
kb add instance athens : City in People
# Facts
kb add fact birthYear(socrates) = 470 in People
kb add fact bornIn(socrates, athens) in People
# Verify and commit everything at once
kb check
kb commit "Added Socrates and basic person/place ontology"
```
---
## 7. Removing Declarations
```bash
kb rm <name>
```
The tool warns if other declarations depend on the one being removed. Remove dependents first.
---
## 8. Reusable Definitions
```bash
kb add def yearsToDouble (r : Float) : Float := Float.log 2 / r in Finance
kb eval "yearsToDouble 0.05"
kb list defs
kb show def yearsToDouble
```
---
## 9. Best Practices
- **Put base types in one domain** (e.g. `Ontology`) so all other domains can import it cleanly.
- **Group by agent-loadable context**: a domain should contain what an agent needs for a specific task.
- **Use meaningful domain names**: `People`, `Physics`, `Finance`, `Geography` — not `Domain1`.
- **Prefer `def` over `axiom` for computed facts** — definitions are safer and evaluable.
- **Run `kb check` once after a batch** of additions, not after each one.
- **Commit with descriptive messages** so the KB history is readable.
---
## 10. Session End Protocol
```bash
kb commit "Session summary: what was added"
kb list all # Review final state
kb domains stats # Confirm counts are as expected
```
---
## 11. Need Help?
```bash
kb help
```
Lean error messages are forwarded directly. A typical error like `unknown identifier 'Person'` means the type was declared in another domain file that hasn't been imported yet — run `kb check` to sync imports, or check that you added the base type before its dependents.
|
