Google Zanzibar datalog lang lets you describe concepts and express how they are related. I generalize it to DSL you can use on Lean4 (and other languages) this lets you represent a knowledge base you can construct, store and evaluate, have it under git and improve without big engines or relaying on external infrastructure.
as a lean noob but a datalog novice, could you explain how it ties to lean? I thought of lean as a proof language rather than a programming language. don't you have to write out every step yourself? or.. hrm. is lean actually a pure functional language with dependent types, and the tactics are just functions? or are tactics like type-level functions, but lean can support regular functions too?
Lean4 core is a functional programming lang and Zil it's a DSL implemented ontop, that means it would define a set of abstractions lean4 accepts such as theorems and lemmas, im also learning !
initial implementation uses clojure, I used claude to port it to Lean4 for my projects, it helps AI agents specially well because it allows it to keep context about how concepts are related and define rules and have a query system(datalog)
to recover. If you try it pls report back ! if doesnt work, just mention how what what was the context, maybe there's a way to improve it for that case too.
cheers and happy hacking.