The thing is that there is a standard format where the definition of the theorem is split from the proof, and verifying that the definition matches the mathemat

The thing is that there is a standard format where the definition of the theorem is split from the proof, and verifying that the definition matches the mathematical concept is a LOT less work then reading the proof, especially if you're willing to assume that definitions in Mathlib are correct.