Lean 4 KnowledgeCheck 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.
Elpi finds. Lean checks.
LeanRDF and lean-elpi form a concrete search-and-check pipeline. A search engine produces a derivation certificate; a verified checker relates accepted certificates to the formal semantics.
Logic programming that understands binders.
LeanElpi is a Lean implementation of the ELPI dialect of λProlog. Use higher-order terms, scoped variables, hypothetical assumptions, and backtracking to express a search. The engine is usable from Lean and through language bindings.
A semantic web stack with formal contracts.
LeanRDF starts with RDF terms, graphs, parsing, and interpretations. RDFS entailment connects rules to their model-theoretic meaning. Above that sit a formalized SPARQL evaluator, OWL 2 RL and EL rules, and a SHACL Core validator.
Relations with roles. Types across the boundary.
typedb-lean connects TypeDB to Lean through typed schemas, queries, results, and transaction modes. Lean structures describe entities and relations; migrations and schema verification help keep the application and live database aligned.
A property graph close to your application.
ladybug-lean provides typed node and relationship tables, checked Cypher, and a common interface for LadybugDB and a pure in-memory backend. It is a practical path for embedded graphs, local experiments, and repeatable tests.
Use the graph your problem needs.
| Foundation | Natural fit | Lean connection | Proof boundary |
|---|---|---|---|
| TypeDB | Rich domain models, role-based relations, shared database | Typed schemas, transactions, and result decoding | Application invariants need explicit proofs |
| LadybugDB | Embedded property graphs, local agent memory, Cypher | Typed graph schema and queries; pure test backend | Typed queries do not certify the native engine |
| RDF / LeanRDF | Shared vocabularies, interoperable data, semantic entailment | Formal interpretations, derivations, and checkers | Guarantees are scoped to the formalized semantics |