I think Kevin Buzzard et al are aiming for a future where big, complicated proofs not accompanied by code are considered suspicious. I wonder if being able to

I think Kevin Buzzard et al are aiming for a future where big, complicated proofs not accompanied by code are considered suspicious. I wonder if being able to drill all the way down on the proof will alleviate much of the torture you mention.