[UltraSane]

I don't quite understand the objection. The 200,000 line Lean proof can be used in other proofs without needing to understand it. This is the biggest advantage of formally verified proofs.