GitHub - lurk-lab/yatima: A zero-knowledge Lean4 compiler and kernel

Yatima is a Lean 4 compiler backend targeting the the Lurk language for recursive zkSNARKs, enabling zero-knowledge proofs of Lean 4 execution. Additionally, Yatima has its own Lean 4 implementation of a kernel for the Lean 4 core language, which can be compiled to Lurk to allow zero-knowledge proofs of Lean 4 typechecking. By verifying a zero knowledge proof that a Lean 4 declaration has passed t

[newnakashima]

∀とかλが構文に入ってるっぽくて大変そうな感じがした

[paulownia]

ディアスポラ・・・

[barlog]

“Yatima: A programming language for the decentralized web”