Proof and beauty.
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....
| Published in: | Economist Vol. 375; no. 8420; pp. 73 - 75 |
|---|---|
| Format: | Article |
| Published: |
Economist Newspaper Limited
4/2/2005
|
| Subjects: | |
| Online Access: | View this record in EBSCOhost |
| fields | @attributes: recordID: 1 pdfLink: plink: https://search.ebscohost.com/login.aspx?direct=true&db=hlh&AN=16607358&site=ehost-live header: @attributes: shortDbName: hlh uiTerm: 16607358 longDbName: Humanities International Complete uiTag: AN controlInfo: bkinfo: jinfo: jid: 00130613 ECO jtl: Economist issn: 00130613 maglogo: N pubinfo: dt: 4/2/2005 vid: 375 iid: 8420 pid: 161 pub: Economist Newspaper Limited artinfo: ui: 16607358 ppf: 73 ppct: 2 formats: tig: atl: Proof and beauty. aug: su: Mathematics problems & exercises Logic Computer reliability Mathematical programming Philosophy of science Mathematicians Computer software History sug: subj: Mathematics problems & exercises Logic Computer reliability Mathematical programming Philosophy of science Mathematicians Computer software History ab: 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. pubtype: Periodical doctype: Article src: R language: English refInfo: copyright: @attributes: flag: Y dt: @attributes: year: 2005 holdings: @attributes: islocal: N |
|---|