# 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 `. Each domain is a `.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 ` at the end. Both `→` and `->` are accepted as type arrows. | Command | Example | |---------|---------| | `add type [extends

] in ` | `kb add type Person extends Entity in People` | | `add instance : in ` | `kb add instance socrates : Person in People` | | `add prop : -> in ` | `kb add prop birthYear : Person -> Nat in People` | | `add rel : -> -> Prop in ` | `kb add rel bornIn : Person -> Place -> Prop in People` | | `add fact in ` | `kb add fact birthYear(socrates) = 470 in People` | | `add rule : in ` | `kb add rule anc : ∀ x y z, parentOf x y → parentOf y z → ancestorOf x z in People` | | `add def : := in ` | `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 ]` | List all declarations, optionally restricted to one domain | | `list types / instances / props / rels / facts / rules / defs [of ]` | Filter by kind | | `show def ` | Print the full Lean source of a declaration | | `get ()` | Retrieve a property value — runs `#eval prop inst` in Lean | | `search ` | Full-text search across declaration names, Lean source, and domain names | | `deps ` | Show what `` uses (forward) and what uses `` (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 `. Run 'help' for usage. ``` Check exit codes in scripts: ```bash kb add type Person in People || echo "Add failed, continuing..." ```