Lean 4 for graph engineers.

A graph becomes easier to reason about when its vocabulary has explicit types. A person and an organization may both have names, but they are different kinds of value. A relation can record that difference.

structure Person where
  name : String

structure Organization where
  name : String

structure Employment where
  person : Person
  organization : Organization

The fields of Employment specify its endpoints. Swapping a person for an organization does not match this structure’s type. In a real database design you would usually store stable identifiers or typed references rather than duplicate entire values.

This model says nothing yet about when someone was employed or whether the source is reliable. Types expose the structure of your claim; the next step is choosing its obligations.

Try it

You want to represent membership in an organization. Which parts are ordinary data, and which might require a rule?

Dependent type theory lets the type of one field refer to another field’s value. That is useful when a valid object must carry evidence of a property of its own data.

structure BoundedCount (limit : Nat) where
  count : Nat
  withinLimit : count ≤ limit

example : BoundedCount 3 :=
  { count := 2, withinLimit := by decide }

BoundedCount 3 is a type. Its proof field refers to the particular count and limit. The example provides both the number and a proof that it satisfies the bound.

For an ontology, the corresponding idea is a store bundled with a proof of a predicate such as Valid store. You must define that predicate, establish an initial valid store, and prove that each permitted update preserves it.

Try it

Does putting a field named valid : Bool into a record provide the same guarantee?

In Lean, propositions are types and proofs are terms. A simple theorem can package a piece of evidence supplied by an assumption.

example (P Q : Prop) (h : P ∧ Q) : P := by
  exact h.left

This proves that P follows from P ∧ Q. It does not establish either proposition without that assumption. The same discipline applies to a graph: a derivation explains what follows from the input and the rules.

Imagine two input claims: a cat is a mammal, and Tom is a cat. A formal rule may justify the conclusion that Tom is a mammal. The proof checks the inference. The source and accuracy of the two input claims remain a separate concern.

Try it

Your agent proves an answer from yesterday’s graph. Is that enough to answer a question about the current graph?

For larger examples, inspect dependencies with Lean’s #print axioms command, avoid unfinished sorry proofs, and understand any native computation used in the checking path.