Ground truth Lean 4 corpus for PMAT proof quality verification — theorems, lemmas, sorry detection, proof completeness metrics - View it on GitHub