@ef-esp
🎊 Grant Announcement: Binius in Lean!
Formalizing Polynomial Commitment Schemes built on Binary Tower Fields, specifically Binius and FRI-Binius, within ArkLib (https://github.com/Verified-zkEVM/ArkLib), Lean's library of formally verifier SNARKs.