Home

Welcome to the yatima-lang wiki!

The end goal of this repository is to:

• Independently evaluate and typecheck Lean 4 programs with both Rust and Lean4 implementations
• Content-address every Lean4 environment, declaration, expression and universe level via using the IPLD data format, with a name-irrelevant representation similar to the Unison language
• Compile Lean programs to the Lurk zkSNARK language, so that we can generate zero-knowledge proof, which can be verified in constant-time and space, that a Lean program f, with input x evaluates to y.
• Compile the Yatima typechecker itself to Lurk, so we can generate zero-knowledge proofs that the Lean program check, with inputs env : Yatima.Environment, const : Yatima.Constant, returns successfully without error. For example, we can produce a cryptographic witness that some definition def foo : M := N correctly typechecks, which can be validated without re-running the typechecker.

This will enable us to produce a succinct and efficiently verifiable correctness certificate for e.g. Lean's mathematical library, mathlib, which currently takes over 4 hours to be compiled (typechecked) by the Lean 3 kernel (as of May '22).