Lean 4 KnowledgeLogic & proof search
lean-elpi
Higher-order logic programming inside Lean. Let λProlog explore the possibilities, then certify the evidence.
Graph engineering meets formal reasoning
Knowledge
worth building
on.
From connected data to certified reasoning. Explore Lean 4, knowledge graphs, and the logic that makes AI agents accountable for their answers.
OPEN-SOURCE PROJECTS · PRACTICAL GUIDES · ONE LOGICAL FOUNDATION
Fig. 01 / The tree of knowledgeFrom claims to evidence
λ Higher-order logic⊢ Kernel-checked proofs◇ Typed knowledge graphs✳ Open-source foundations
The ecosystem
Four projects. A shared idea.
The semantic stack
LeanRDF
From RDF triples to formal entailment. Semantics, search, and checked certificates for the semantic web.
Typed knowledge graphs
typedb-lean
Bring TypeDB’s rich relationships into Lean, with typed schemas, transactions, queries, and results.
Embedded property graphs
ladybug-lean
A local graph, a typed schema, and checked Cypher. Build with LadybugDB or a pure in-memory backend.
A map of the territory
From graphs to guarantees.
Storage, semantics, search, and checking each have a job. Select a layer to see where it belongs.
05
Check against the foundation.
Lean’s dependent type theory lets propositions be types and proofs be terms. The kernel checks proof terms against their claimed types, relative to the definitions and axioms used.
Learn dependent types ↗A conceptual map of responsibilities, not a single installed product. Database adapters are alternatives; connecting stored facts to proof obligations is application work.
The book behind the work
Bulletproof
Knowledge.
Build hallucination-resistant neurosymbolic agents with Lean and logic programming. A practical journey from typed ontologies to memory and answers backed by checked evidence.
Field notes
Ideas you can put to work.
When your knowledge carries its own proof
Move from a graph that stores claims to an interface that requires evidence for the invariants you care about.
Let logic search. Let Lean check.
Higher-order terms make binders and relations first-class. Certificates separate finding an answer from trusting it.
The semantic stack, with evidence at every boundary
RDF, RDFS, SPARQL, OWL profiles, and SHACL answer different questions. LeanRDF gives those questions explicit semantics.
The learning corner
A little theory.
A lot to build.
Start with types and proofs. Add logic programming. Then bring the ideas to a real graph.
Find your learning path ↗
Built by Volodymyr Pavlyshyn.
Software architect, author, and builder of knowledge systems.