QED

David Corfields blog wees me op een interessant interview met de wiskundigen Gian-Carlo Rota en David Sharp: “Mathematics, Philosophy, and Artificial Intelligence”, Los Alamos Science, No. 12 (1985). Op pagina 99 vertelt Rota over een aantal belangrijke combinatorische problemen en hij verwijst naar de vierkleurenstelling, die hij bewust vierkleurenvermoeden noemt:

The four-color conjecture –that with only four colors you can color every planar map so that no two adjacent regions have the same color– is one of these critical problems.

Sharp onderbreekt hem:

I thought that had been settled by a computer proof.

Rota antwoordt dan waarom hij het computerbewijs door Appel, Haken en Koch geen bewijs vindt:

Not really. What we want is a rational proof. It doesn’t help to have a brutally numerical answer spewed out by a computer. A problem is interesting only when it leads to ideas; nobody solves problems for their own sake, not even chess problems. You solve a problem because you know that by solving the problem you may be led to see new ideas that will be of independent interest. A mathematical proof should not only be correct, but insightful. Although, as Erdös says, nobody gets blamed if his first proof is messy.

Anno 2007 zijn alle bekende bewijzen van de vierkleurenstelling nog altijd gebaseerd op computerberekeningen. Rota zou de stelling nu dus nog altijd een vermoeden noemen.