What is Lean?

What are zk-SNARKS? (Or some other version of this)

zkPi intro

Show benchmark figure here

Explain we're missing Strings, Inductive Families, Quotient Types, and Eta-Expansion

Adding strings:

They're stored as .lit "string", but proofs need them to be an inductive type

Solution: Convert to inductive type using String.ofList

Slow speed

Adding quotients:

Explain quotients

Explain changes

Speed: Fine

Inductive families:

Explain them

Explain rule changes briefly

Also works fine

Summary:

Strings suck, everything else was fine

Future work:

Eta-Expansion, larger optimizations on the structure, etc. etc.