Computer proofs

I just read this opinion of Doron Zeilberg. The questions he poses are deep, they date since the age of Aristotle (of course the computers back then did not have today’s capabilities, but non-the-less questions like “what constitutes a proper proof” existed) and it is interesting to argue against and in favor of them. Consider for instance this part:

 If humans will keep trying to find human proofs, and fail, it will raise the probability that 4CT is indeed deep. On the other hand, if some human will prove 4CT tomorrow, only with pencil-and-paper, then this would be very nice for the prover, who will become instantly famous, but very depressing for our mathematical culture as a whole. It would mean that perhaps we humans are so trivial that we are not even capable of stating and conjecturing deep results.

My personal opinion is along the lines of Yair Caro’s opinion which you can read here.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: