Systematic workflows for Lean 4 proofs: sorries management, mathlib usage, verified math, compiler-guided repair