Branch Number Formalization

This project formalizes Theorem 1 from A New Algorithm for Computing Branch Number of Non-Singular Matrices over Finite Fields in Lean 4.

Setup

Install and set up leanblueprint. Note: leanblueprint requires graphviz to be installed first. See the leanblueprint documentation for system requirements before proceeding.

pip install leanblueprint

Useful Commands

Build and serve the blueprint locally:

leanblueprint web
leanblueprint serve

Then visit http://0.0.0.0:8000/ in your browser.

Build the PDF version:

leanblueprint pdf

Build the Lean code:

lake exe cache get  # Download Mathlib cache (recommended)
lake build          # Build the project