Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:A Very Mathematical Dilemma
Authors: Alan Bundy
Date: 2006
Publication Title:The Computer Journal
Publication Type:Journal Article Publication Status:Published
Volume No:49(4) Page Nos:480-486
Mathematics is facing a dilemma at its heart: the nature of mathematical proof. We have known since Church and Turing independently showed that mathematical provability was undecidable, that there are theorems whose shortest proofs are enormous. Within the last half century we have discovered practical examples of such theorems: the classification of all finite simple groups, the Four Colour Theorem and Kepler's Conjecture. These theorems were only proved with the aid of a computer. But computer proof is very controversial, with many mathematicians refusing to accept a proof that has not been thoroughly checked and understood by a human. The choice seems to be between either abandoning the investigation of theorems whose only proofs are enormous or changing traditional mathematical practice to include computer-aided proofs. Or is there a way to make large computer proofs more accessible to human mathematicians?
Links To Paper
1st Link
2nd Link
Bibtex format
author = { Alan Bundy },
title = {A Very Mathematical Dilemma},
journal = {The Computer Journal},
publisher = {OUP},
year = 2006,
volume = {49(4)},
pages = {480-486},
doi = {10.1093/comjnl%2Fbxl021},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh