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 Lean 4 implementations
• Content-address every Lean 4 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 3 hours to be compiled (typechecked) by the Lean 3 kernel (as of May '22).

To strengthen the motivation for the example above, Mathlib grows not only in terms of SLOC, but also in terms of contributions (and contributors!). As more and more mathematicians engage in this endeavor, more branches are created and more PRs are open, leading to an ever-growing computational cost. And as one may wonder, there's certainly a considerable chunk of overlapping computation going on among those branches. Now imagine how much of that cost can be cut off if we're able to trust on proof terms without triggering the kernel twice for the same computation.