Install Python 3, Git, and Lean with elan: https://lean-lang.org/install/
In this extracted folder run:

python3 prepare.py
lake env lean -DwarningAsError=true Kaczmarz.lean

Lean and Mathlib are pinned to 4.33.1; lake-manifest.json pins all dependency commits.
The first setup downloads compiled dependencies from the Mathlib cache.
Each file covers selected results, not a complete paper. Read its scope and assumptions.
Prior-work searches do not certify first-formalization status.
