Lemma

Lemma

Lemma: A blockchain platform where users post unsolved mathematical theorems with bounties, and solvers submit proofs for on-chain validation and trustless rewards.

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.

Tracks Applied (4)

Prizes for Top 3, Hackers' Choice & Chewing Glass

Lemma qualifies as a top contender for ZK Hack Montréal prizes by innovatively applying ZK technology to mathematics. It...Read More

🤩 Best zkVM Application

We've built an app that we believe and solve a very real and very important problem - decentralized and trustless market...Read More

RISC Zero

🤝 ZK Coprocessor

"you're probably the first ones to do this" ~Nuke, RISC-0 Team Member referring to using Bonsai from the browser for se...Read More

RISC Zero

👪 Integrations Bounty

We integrated a complex mathematical theorem proving system with the RISC-0 proving system and Bonsai coprocessor.

RISC Zero

Discussion