Show HN: Lean4 Datalog DSL Based on Google Zanzibar for AI Projects (github.com)

18 points by kbradero 1mo ago ↗ HN

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...

1 comment of 2

[ 1.7 ms ] story [ 9.5 ms ] thread

sterlind 1mo 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?