| Sumario: | The article discusses the role of computers in producing mathematical proofs. Through much of the 20th century, questions of mathematical rigour were passed off to logicians and philosophers--working mathematicians have been, for the most part, content to work with an intuitive definition of proof. This notion works when each step of a proof is transparent, and can be examined by all. Proof is then just a process of reducing one big, non-obvious step, to a bunch of small, obvious ones. However, if a computer is used to make this reduction, then the number of small, obvious steps can be in the hundreds of thousands--impractical even for the most diligent mathematician to check by hand. Critics of computer-aided proof claim that this impracticability means that such proofs are inherently flawed. Formal proof is a notion developed in the early part of the 20th century by logicians such as Bertrand Russell and Gottlob Frege, along with mathematicians such as David Hilbert (who can fairly be described as the father of modern mathematics) and Nicolas Bourbaki, the pseudonym of a group of French mathematicians who sought to place all of mathematics on a rigorous footing. The benefit of formal logic is that it is pure syntax. At no point does proceeding from one step to the next require understanding, let alone mathematical intuition. It is possible that mathematicians will trust computer-based results more if they are backed up by transparent logical steps, rather than the arcane workings of computer code, which could more easily contain bugs that go undetected.
|
|---|