path: root/README.md

# 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**: stored as `.lean` files in a Git repository — survives across 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.

---

## Planned Domain Structure

The KB is organised into four top-level sections, each subdivided into domain files that correspond to a specific area of knowledge. The subsections are the natural unit an agent loads — for example, loading only `Physics` or only `MoneyFinance` without pulling in unrelated facts.

### Mathematics

| Domain file | Coverage |
|-------------|----------|
| `ElementaryMath` | Arithmetic, fractions, percentages; reasoning about 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, continuity, domain & range |
| `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, number-theoretic, representation formulas |

### Science & Technology

| Domain file | Coverage |
|-------------|----------|
| `Physics` | Mechanics, oscillations & waves, statistical physics, thermodynamics, electricity & magnetism, optics, relativity, nuclear, quantum, particle, astrophysics, constants, principles, effects, fluid mechanics |
| `Chemistry` | Matter from atoms and ions to biomolecules |
| `UnitsMeasures` | Conversion and analysis of scientific and everyday measurement systems |
| `Engineering` | Aerospace, energy, electrical, control systems, mechanical, civil, fluid mechanics, acoustics, steam tables, measurement devices |
| `ComputationalSciences` | Cellular automata, substitution systems, Turing machines, complexity, algebraic codes, fractals, image processing, hashing |
| `EarthSciences` | Geology, geodesy, oceanography, climatology |
| `LifeSciences` | Human anatomy, animal anatomy, neuroscience, genomics, molecular biology, animals and plants |
| `SpaceAstronomy` | Phenomena and technology beyond Earth's atmosphere |

### Society & Culture

| Domain file | Coverage |
|-------------|----------|
| `People` | Biographical and demographic data on notable individuals and public figures |
| `ArtsMedia` | Music, films, comics, sculptures, paintings, and related media |
| `History` | Timelines, monetary value analysis, historical events, inventions, conflicts |
| `WordsLinguistics` | Word properties, languages, document length, notable texts, transliterations, Morse code, Soundex, encodings, emotions |
| `MoneyFinance` | Stock data, mortgages & loans, salaries, bonds, derivative valuation, income tax, sales tax |
| `DatesTimes` | Dates, calendars, time systems |
| `FoodNutrition` | Nutritional data and dietary guidelines |
| `Demographics` | Health care, age/sex, gender equality, business, citizenship, crime, education, income & employment, language, race, marriage, mobility, 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, gasoline, food, electricity prices |
| `Entertainment` | Music, films, artworks, cultural productions |
| `HouseholdScience` | Scientific reasoning applied to everyday physical phenomena |
| `HouseholdMath` | Everyday calculations and measurements |
| `Programming` | Algorithms, data structures, programming concepts |
| `Hobbies` | Recreational activities and personal projects |
| `TodaysWorld` | World economy, Finland economy, weather |

---

## Knowledge Representation

| Kind | Description | Lean form |
|------|-------------|-----------|
| **Type** | A category or class | `opaque Person : Type` |
| **Subtype** | A type extending another | `opaque Philosopher : Type` + coercion axiom |
| **Instance** | A named individual | `opaque socrates : Person` |
| **Property** | A function from a type to a value | `opaque birthYear : Person → Nat` |
| **Relation** | A binary predicate | `opaque bornIn : Person → Place → Prop` |
| **Fact** | An asserted value or relation | `axiom fact_birthYear_socrates : birthYear socrates = 470` |
| **Rule** | A universally quantified axiom | `axiom ancestors_transitive : ∀ x y z, …` |
| **Definition** | A named computable expression | `def yearsToDouble (r : Float) : Float := …` |

---

## 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.

### Inspecting knowledge

| Command | Description |
|---------|-------------|
| `list <types\|instances\|props\|rels\|facts\|rules\|defs\|all> [of <Domain>]` | List declarations, optionally filtered by domain |
| `show def <n>` | Print the Lean source of a declaration |
| `domains` | List all domains active this session with declaration counts |
| `domains stats` | Detailed breakdown per domain and kind |

### Querying

| Command | Description |
|---------|-------------|
| `eval <expr>` | Evaluate a computable Lean expression via `#eval` |
| `query <prop>` | Attempt to prove a proposition (Yes / No / Unknown) |

### 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 session summary |
| `rm <n>` | Remove a declaration (warns about dependents) |

---

## 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 at the end rather than after each individual addition.

---

## Example Workflow

```bash
# Initialise
kb init ./myKB
cd myKB

# Base types shared across domains
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

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

# Agent loads only the People domain for a biographical query
kb list all of People
```

---

## Query Capabilities

- **Computational**: `kb eval "yearsToDouble 0.05"` — runs `#eval` on any computable Lean expression.
- **Logical**: `kb query "even (2 + 2)"` — attempts to prove the proposition using `decide`, `aesop`, or `simp`.
- **Selective loading**: `kb list all of Physics` — an agent pulls only the Physics domain into its context for a focused query.

---

## Extensibility

- Domain files from the planned structure are created on first use — no separate setup step.
- Definitions (`kb add def`) become permanent reusable shortcuts stored in Lean files.
- The KB grows incrementally across sessions — each `kb commit` is a checkpoint in Git history.