|Kokkuvõte||SNARKs (and similar cryptographic objects) are non-interactive proofs
that have an extremely efficient verification method. For example,
with the Pinocchio system allows any proof will have a length of at
most 288 bytes, and verification takes only a few milliseconds, no
matter how complex the statement that is to be verified.
The goal of this thesis is to use existing software for SNARKs and to
use it to encode full-fledged mathematical proofs (i.e., proofs of
mathematical theorems verified in some proof-assistant like
Isabelle/HOL) as efficiently verifiable snippets.