Expander Graphs

A Lean 4 project depending on mathlib.

Goal is to formalize Expander Graphs and related Spectral Graph Theory results. Link to the blueprint of the project.

Prereqs

You need elan installed.

Building

git clone https://github.com/celioboulay/expander-graphs.git
cd expander-graphs
lake exe cache get
lake build