Note: This repository is a copy of the template for blueprint-driven formalization projects in Lean 4 provided here.
This is a Lean 4 project that aims to provide a formal blueprint for the soundness of the FRI protocol. The blueprint page can be found here.
The project is not being actively worked on, but is meant to follow the proof of Theorem 8.2 of "Proximity Gap for Reed-Solomon Codes" by Ben-Sasson et al. Ideally, I would like a blueprint with all the theorems and definitions from that paper, as well as from any other papers that this one references for critical lemmas (such as the Polischuk Spielman result).
