Claude did not find a proof, though. It found an algorithm which Knuth then proved was correct.