Lean formalization of "A Simplified Round-by-round Soundness Proof of FRI"

Lean4 formalization of "A Simplified Round-by-round Soundness Proof of FRI" by Albert Garreta (Nethermind Research), Nicolas Mohnblatt (zkSecurity), and Benedikt Wagner (Ethereum Foundation).

Paper: https://eprint.iacr.org/2025/1993

Most of the formalization was done by Harmonic's Aristotle. Claude Opus-4.5 and Sonnet-4.5 were useful in the last stages too. This README was mostly generated by GLM-4.7, provided for free by opencode ZEN.

Project Structure

The formalization follows mathlib conventions with modules organized by topic:

• SimpleRbrFri/Core.lean - Core FRI definitions (distance metrics, folding, Reed-Solomon codes)
• SimpleRbrFri/State.lean - State tracking, canonical bad events, and domain size properties
• SimpleRbrFri/FoldingSoundness.lean - Folding phase soundness (Lemma 5.1)
• SimpleRbrFri/QuerySoundness.lean - Query phase analysis and agreement propagation (Claim 5.3)
• SimpleRbrFri/Soundness.lean - Main round-by-round soundness theorem (Theorem 5.2) ⭐
• SimpleRbrFri/Completeness.lean - Honest prover algorithm and perfect completeness proof
• SimpleRbrFri.lean - Top-level aggregator (import this to access all definitions)

Status

The main round-by-round soundness theorem (Theorem 5.2) has been formalized as FRI_RBR_Soundness in SimpleRbrFri/Soundness.lean. The theorem establishes:

• Folding rounds: Error bounded by err*(C_i, m_i, δ*) (Lemma 5.1)
• Query round: Error bounded by (1 - δ*)^t (Claim 5.3)

The perfect completeness theorem has been proven as FRI_Perfect_Completeness in SimpleRbrFri/Completeness.lean, showing that honest provers always convince the verifier.

Lemma 2.5 has not been formalized. This lemma is useful for instantiating the described protocol. Lemma 2.5 is proven in the WHIR paper by Arnon, Chiesa, Fenzi and Yogev.

There's a possibility that the content of this repository may become polished enough so that some of it can be added to Arklib.

Getting Started

Step 1: Install VS Code

If you don't have Visual Studio Code installed, download and install it from https://code.visualstudio.com/.

Step 2: Install the Lean 4 VS Code Extension

1. Open VS Code
2. Click on the Extensions icon in the left sidebar (or press Ctrl+Shift+X on Windows/Linux or Cmd+Shift+X on macOS)
3. Search for "Lean 4"
4. Click "Install" on the extension by "leanprover"
   • Alternatively, visit Lean 4 VS Code Marketplace

Step 3: Complete the Lean 4 Setup

1. The Lean 4 extension will guide you through installation
2. Click the ∀ symbol at the top right of the VS Code window
3. Select "Show Setup Guide" if it doesn't appear automatically
4. Follow the on-screen instructions to install:
   • Elan: Lean's version manager (similar to nvm for Node.js or pyenv for Python)
   • Lean 4: The Lean compiler and tools

The setup wizard will automatically install Elan and Lean 4 for your operating system.

Step 4: Open This Project

1. In VS Code, go to File > Open Folder...
2. Navigate to and select the folder containing this README.md
3. Click "Select Folder"

Step 5: Download Dependencies

This project depends on mathlib and other Lean libraries. To speed up compilation, download pre-built dependencies:

lake exe cache get

This command downloads cached builds of dependencies, which can save hours of compilation time on first build.

Step 6: Explore the Formalization

In VS Code, you can start by opening:

• SimpleRbrFri/Soundness.lean - Start here to see the main soundness theorem (FRI_RBR_Soundness)
• SimpleRbrFri.lean - Main entry point that imports all FRI modules

VS Code will automatically start checking the Lean code in the background. You should see:

• Syntax highlighting
• Type information on hover
• Goal states when placing cursor in proof positions
• Orange side-bars for checked-in-progress work, double-check marks for checked lemmas

Reading Guide:

1. Start with Soundness.lean to see the main theorem statement (Theorem 5.2)
2. Read FoldingSoundness.lean for folding phase details (Lemma 5.1)
3. Read QuerySoundness.lean for query phase details (Claim 5.3)
4. Compare with Completeness.lean for the completeness direction

Building the Project

To build the entire project manually:

lake build

Troubleshooting

"elan: command not found": Restart your terminal or VS Code after installing Elan. You may need to add Elan to your PATH.

"unknown package" errors: Make sure you've run lake exe cache get and allowed time for dependencies to download.

Slow initial loading: The first time you open a Lean file, it may take several minutes to compile dependencies. Subsequent builds will be much faster.

Learning Lean 4

If you're new to Lean 4, here are some helpful resources:

• Official Lean 4 Documentation
• Mathematics in Lean
• Lean Community