# kb — Lean 4 Knowledge Base CLI

A persistent, formally verified knowledge base stored as a Git repository of Lean 4 files. Every declaration is type-checked by Lean's kernel. An LLM agent interacts with it entirely through the `kb` CLI.

---

## Core Concepts

- **Persistent**: state is stored as `--@kb` metadata comments in each domain file and reloaded automatically on startup — no state is lost between sessions.
- **Formally verified**: every addition is type-checked by Lean's kernel at `kb check` / `kb commit` time.
- **Domain-organised**: declarations are grouped into named domain files. Each domain is one `.lean` file. An agent can load a specific domain into its context without loading the entire KB.
- **Version-controlled**: full history, branching, and reproducibility via Git.
- **Agent-friendly**: all commands return exit code `0` on success and `1` on error, with structured one-line error messages.

---

## Persistence Model

Every declaration written to disk is preceded by a metadata header:

```
--@kb kind=prop name=birthYear domain=People
opaque birthYear : Person → Nat
```

On startup, `kb` scans all `*.lean` domain files in the current directory, parses these headers, and reconstructs the full declaration list. This means:

- Restarting `kb` is safe — all prior work is reloaded.
- The `--@kb` format is the source of truth; the Lean code is preserved exactly for the compiler.
- `rm` removes the entire `--@kb` block and its Lean source atomically, regardless of how many lines the source spans.

---

## Planned Domain Structure

The KB is organised into four top-level sections. Each subsection is one domain file — the natural unit an agent loads for a focused task.

### Mathematics

| Domain file | Coverage |
|-------------|----------|
| `LogicSetTheory` | Boolean algebra, set theory, transfinite numbers |
| `Probability` | Games of chance, Bernoulli's trials, probability formulas and distributions |
| `AppliedMathematics` | Optimization, numerical analysis, dynamic systems, fractals, game theory, packing |
| `ElementaryMath` | Arithmetic, fractions, percentages; parity and sign of underspecified values |
| `Algebra` | Variables, number systems, algebraic operations and symbols |
| `Geometry` | Plane, solid, coordinate, transformations, high-dimensional, packing, curves, polyforms, topology, tilings |
| `Plotting` | Functions, equations, parametric plots, inequalities, number lines, polar plots |
| `Calculus` | Integrals, derivatives, limits, sequences, products, series, sums, vector analysis, transforms |
| `DifferentialEquations` | Ordinary (ODE) and partial (PDE) differential equations |
| `Statistics` | Descriptive statistics, inference, regression, random variables |
| `Functions` | Domain & range, injectivity, surjectivity, continuity, periodic, odd/even, special functions |

### Science & Technology

| Domain file | Coverage |
|-------------|----------|
| `Physics` | Mechanics, thermodynamics, electromagnetism, optics, relativity, nuclear, quantum, particle, astrophysics, fluid mechanics, physical constants |
| `Chemistry` | Elements, molecules, ions, quantities, reactions, thermodynamics, solutions, quantum chemistry, bonds & orbitals, nuclear chemistry |
| `UnitsMeasures` | Conversion and analysis of scientific and everyday measurement systems |
| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables |
| `HealthMedicine` | Anatomy, medical codes, blood alcohol, mortality, diseases, medical computations, drugs, public health |
| `TechnologicalWorld` | Communications, satellites, barcodes, space probes, nuclear power, carbon footprint, inventions, web & computer systems |
| `Materials` | Alloys, bulk materials, hardness, minerals, plastics, woods, material chemistry |
| `ComputationalSciences` | Cellular automata, Turing machines, complexity, algebraic codes, fractals, image processing, hashing |
| `EarthSciences` | Geology, geodesy & navigation, oceanography, atmospheric sciences, climate |
| `LifeSciences` | Human anatomy, animal anatomy, neuroscience, genomics, molecular biology, animals and plants |
| `SpaceAstronomy` | Phenomena and technology beyond Earth's atmosphere |
| `FoodScience` | Food composition, nutrition, dietary standards, food physics |

### Society & Culture

| Domain file | Coverage |
|-------------|----------|
| `Education` | International education, universities, school districts, standardized tests |
| `People` | Biographical and demographic data on notable individuals and public figures |
| `ArtsMedia` | Movies, television, video games, notable texts, periodicals, comics, mythology, music |
| `History` | Historical periods, genealogy, events, countries, military conflicts, world leaders, inventions |
| `WordsLinguistics` | Word properties, languages, transliterations, Morse code, Soundex, encodings |
| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income and sales tax |
| `DatesTimes` | Dates, calendars, time systems |
| `FoodNutrition` | Nutritional data and dietary guidelines |
| `Demographics` | Health care, age/sex, gender, education, income, crime, marriage, religion, military, HDI |

### Everyday Life

| Domain file | Coverage |
|-------------|----------|
| `PersonalHealth` | Physical exercise, food and nutrition, child growth & development |
| `PersonalFinance` | Mortgages & loans, stock data, currency conversion, cost of living, prices |
| `Entertainment` | Music, films, artworks, cultural productions |
| `HouseholdScience` | Scientific reasoning applied to everyday physical phenomena |
| `DatesAnniversaries` | Calendar information, celebrations, time zones, anniversaries |
| `Travel` | Weather, cost of living, flight data, gasoline prices, points of interest |
| `HouseholdMath` | Everyday calculations and measurements |
| `Programming` | Algorithms, data structures, programming concepts |
| `Hobbies` | Recreational activities and personal projects |
| `TodaysWorld` | World economy, Finland economy, weather |

---

## CLI Commands

### Adding knowledge  *(all require `in <Domain>`)*

| Command | Description |
|---------|-------------|
| `add type <n> [extends <Parent>] in <D>` | Declare a type, optionally as a subtype |
| `add instance <n> : <Type> in <D>` | Declare a named individual |
| `add prop <n> : <DomType> -> <Range> in <D>` | Add a property |
| `add rel <n> : <D1> -> <D2> -> Prop in <D>` | Add a binary relation |
| `add fact <fact> in <D>` | Assert a fact: `prop(inst) = val` or `rel(a, b)` |
| `add rule <n> : <statement> in <D>` | Add a universally quantified axiom |
| `add def <n> <params> : <Type> := <body> in <D>` | Define a reusable computed shortcut |

Both `→` (Unicode) and `->` (ASCII) are accepted as type arrows.

### Reading knowledge

| Command | Description |
|---------|-------------|
| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations |
| `show def <n>` | Print the Lean source of a declaration |
| `get <prop>(<inst>)` | Retrieve a property value — runs `#eval prop inst` |
| `search <text>` | Full-text search across names, Lean source, and domain names |
| `deps <n>` | Show forward dependencies (what `<n>` uses) and reverse dependencies (what uses `<n>`) |
| `eval <expr>` | Evaluate a Lean expression via `#eval` |

### Querying

| Command | Description |
|---------|-------------|
| `query <prop>` | Attempt to prove a proposition. Returns `Status: Yes/No/Unknown`. |
| `query <prop> using <tactic-script>` | Same with a custom tactic. On success, prints the proof term. |

Default tactic sequence: `first | decide | aesop | simp`.

Useful custom tactics:
- `decide` — fully decidable propositions
- `native_decide` — faster for large decidable computations
- `omega` — linear arithmetic over `Nat` and `Int`
- `norm_num` — numeric computations
- `ring` — ring equalities
- `simp [myLemma]` — simplification with specific lemmas

### Build and version control

| Command | Description |
|---------|-------------|
| `init <dir>` | Create a new KB repository |
| `check` | Sync imports and run `lake build` to verify the whole KB |
| `commit <message>` | Verify then `git commit` all changes |
| `status` | Show `git status` and domain summary |
| `rm <n>` | Remove a declaration and its metadata block (warns about dependents) |

### Domain info

| Command | Description |
|---------|-------------|
| `domains` | List all loaded domains with declaration counts |
| `domains stats` | Detailed breakdown per domain and kind |

---

## How `check` Works

`kb check` does three things before running `lake build`:

1. Scans the KB root for all `*.lean` domain files.
2. Inspects which domains reference names declared in other domains, and injects the necessary `import` lines.
3. Rewrites `KnowledgeBase.lean` to import all domain files so `lake build` compiles everything.

Add a batch of declarations, then run `check` once — not after each individual addition.

---

## Exit Codes

Every command exits with `0` on success and `1` on error (duplicate declaration, name not found, build failure, parse failure). This allows agent scripts to detect failure without parsing output:

```bash
kb add type Person in People && echo "OK" || echo "FAILED"
```

---

## Example Workflow

```bash
kb init ./myKB && cd myKB

# Add a batch
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
kb add prop birthYear : Person -> Nat in People
kb add rel bornIn : Person -> Place -> Prop in People
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          # forward and reverse dependency graph
kb search athens           # full-text search
kb get birthYear(socrates) # → 470

# Query
kb query "birthYear socrates = 470" using decide
# Status: Yes
# Proof: ...

# Verify and persist
kb check
kb commit "Added Socrates and basic person/place ontology"

# Next run: all state reloads automatically from People.lean
```