Use Lean 4.19.0 and Mathlib revision c44e0c8ee63ca166450922a373c7409c5d26b00b. Python 3.13 uses only its standard library for the included build driver and exhaustive evaluator. Extract the package. Set root to the extraction directory, workspace to your Mathlib checkout, lake to your Lake executable, threads to 1 and workers to 2 in verification/lean_build.yaml. Run python verification/build_lean.py --config verification/lean_build.yaml. This compiles CircuitSpec, Core, all eight case modules, Solution and LeanProof. Inspect the printed theorem axiom dependencies. Proof/Solution.lean exports the complete solution, importing its supporting modules. The reference circuit has 64 AND gates and 316 total gates. Compare the Lean circuit literal and JSON gate list under the supplied wire semantics. Existing logs record the completed author verification; rebuild from source for independent verification.
