From 34fedb615f7a2ee809ec098c45f362f7933ae138 Mon Sep 17 00:00:00 2001 From: sukrucildirr Date: Sat, 10 May 2025 17:06:04 +0300 Subject: [PATCH] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3cfea6fb..9102d6ae 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # yatima -Yatima is a Lean 4 compiler backend targeting the [the Lurk language](https://lurk-lang.org/) for recursive zkSNARKs, enabling zero-knowledge proofs of Lean 4 execution. +Yatima is a Lean 4 compiler backend targeting the [the Lurk language](https://docs.argument.xyz/) 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 the typechecker, one can verify that the declaration is type-safe without re-running the typechecker.