You could feed the proof to a (simple, verified) proof checker rather than check it by hand. Then you only need to check the statement that was proven was the o

You could feed the proof to a (simple, verified) proof checker rather than check it by hand. Then you only need to check the statement that was proven was the one you wanted, without having to vet the code that spits out the proof line by line (until you actually hit a bug and the proof fails to check). I don't think it would be inconceivable for mathematica to implement something like that, though perhaps it's not really their core business.