# 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 `. Each domain is stored as a separate `.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 ` at the end. | Command | Purpose | Example | |---------|---------|---------| | `kb add type [extends ] in ` | Declare a type | `kb add type Person extends Entity in Ontology` | | `kb add instance : in ` | Declare an individual | `kb add instance socrates : Person in People` | | `kb add prop : -> in ` | Declare a property | `kb add prop birthYear : Person -> Nat in People` | | `kb add rel : -> -> Prop in ` | Declare a relation | `kb add rel bornIn : Person -> Place -> Prop in People` | | `kb add fact in ` | Assert a fact | `kb add fact birthYear(socrates) = 470 in People` | | `kb add rule : in ` | 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 : := in ` | 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 ` | Compute a value | `kb eval "yearsToDouble 0.05"` | | `kb query ` | Ask if a proposition is provable | `kb query "even (2 + 2)"` | | `kb list all of ` | 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 ``` 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.