Add reproducible Lean formal verification workflow

.flake8

@@ -1,3 +1,5 @@
 [flake8]
 max-line-length = 200
 ignore = E203, F811, W503, W605
+per-file-ignores =
+    formal_verification/python/generate_current_run.py:E231

.gitignore

@@ -72,5 +72,17 @@ docs/build
 mlruns
 geopi_tracking
 
+# Local scratch / render QA output
+tmp/
+
+# Local verification environments and research-only inputs
+.venv-lean/
+Lean_verification_docs/
+
+# Local development-tool state (not part of the product)
+.codegraph/
+.*_work/
+
+# Local generated multiclass artifacts
 multiclass_classification
 multiclass_cli_test.csv