Lean 4 KnowledgeLearn the language.
Types, structures, propositions, and small proofs. Start with our Lean course, then open the official books.
Learn to reason.
Use λProlog to describe a search. Learn what binders and hypothetical assumptions make possible.
Bring a graph.
Choose a data model. Read its mini-book, run the project examples, and identify the claim you want to certify.
The resource library.
14 resourcesLean 4 for graph engineers
From a domain model to a dependent type and a proof obligation. Includes short exercises and worked answers.
Start reading ↗ELPI & higher-order reasoning
Relations, binders, local assumptions, and the bridge from a search result to evidence.
Start reading ↗LeanElpi: λProlog in Lean 4
Learn the language, engine, Lean integration, bindings, and optional certification layer.
Start reading ↗RDF semantics in Lean 4
Move from triples and interpretations to certificates, SPARQL, OWL, and SHACL.
Start reading ↗Typed Graphs: TypeDB and Lean Together
Seven chapters covering TypeDB, Lean basics, domain models, typed transactions, and an application.
Start reading ↗LadybugDB & Lean
Property graphs, typed ontologies, Cypher, and the Lean companion library.
Start reading ↗Theorem Proving in Lean 4
Dependent type theory, propositions, quantifiers, tactics, inductive types, and axioms.
Start reading ↗Functional Programming in Lean
Learn Lean as a programming language, including data, effects, and dependent types.
Start reading ↗Mathematics in Lean
Practice proof construction using Lean and Mathlib through worked mathematical examples.
Start reading ↗The ELPI manual
The upstream interpreter’s syntax, semantics, higher-order terms, constraints, and embedding APIs.
Start reading ↗RDF 1.1 Semantics
The primary model-theoretic reference behind RDF and RDFS entailment.
Start reading ↗Bulletproof Knowledge
A full path through typed ontologies, agent memory, higher-order reasoning, and checked evidence.
Start reading ↗TypeDB for Edge AI Agents
Go deeper into typed knowledge graphs as the memory of an AI agent.
Start reading ↗LadybugDB for Edge Agent AI Memory
Explore property graphs, metagraphs, and embedded agent memory.
Start reading ↗No matching resources. Try another search or select All.