The question came up of how one validated a proof involving computers. I've heard that this was not an abstract problem: programming bugs were found in the program but then it was shown that the bugs did not affect the result.
I'm not sure whether anyone has independently written and run a program to verify the output.
Cheers,
Ben