Show HN: Lean4 Datalog DSL Based on Google Zanzibar for AI Projects

kkbradero about 10 hours ago 2 commentsRead Article on github.com

ZH version is available. Content is displayed in original English for accuracy.

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.

Google's Zanzibar paper: https://storage.googleapis.com/gweb-research2023-media/pubto...

⚡ Community Insights

Discussion Sentiment

100% Positive

Analyzed from 147 words in the discussion.

Discussion (2 Comments)Read Original on HackerNews

sterlind•about 7 hours ago

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?

kbradero•about 6 hours ago

Lean4 tactics are related to Clojure/Lisp based macros (https://lean-lang.org/theorem_proving_in_lean4/Tactics/)

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.