The problem Lemma solves

Lemma is a ZK theorem proving framework that enables individuals to post unsolved theorem definitions accompanied by a bounty for anyone that can submit a valid Mathematical proof which solves the theorem. These proofs are validated on chain, and the bounties are trustlessly released to the solver.

Challenges we ran into

Caching issues with RISC-0

The Risc0 forge template caches a lot of data under the hood. As a result we've run into a few instances where one team member deploying the smart contract was using a different version of the ELF binary then the team member deploying a different piece of our project. Which resulted in invalid proofs

Math

We've tackled this issue without fully understanding the theory behind formal verification systems. None of us have a strong math background - when diving into Lean4/proost concepts like Dependent Type Theory or Calculus of Construction flew right over our heads.

Compiling proost for RISC-0

A significant portion of our hacking time was spent getting proost to compile to the RISC-0 target - Many aspects of Proost are incompatible with the RISC-0 zkVM due to unsupported sys calls and required us to massage the code base into a more compatible form.

CORS issue with Bonsai

We wanted the project to just work - meaning we didn't want to force the user to run a CLI locally, instead relying solely on the browser validated by their Metamask wallet. This ended up being more difficult than expected as Bonsai doesn't handle CORS headers correctly. We had to implement a relaying service that accepts our requests and routes them to Bonsai.