Computerbewijzen in de wiskundige praktijk

Koen
Vervloesem

Gaan computers wiskundigen vervangen?



'Een wiskundige is een machine om koffie in stellingen om te zetten,' zei de Hongaarse wiskundige Paul Erdös ooit. Zo vanzelfsprekend is het bewijzen van wiskundige vermoedens echter niet. Naast koffie vergt het ook veel bloed, zweet en tranen en soms honderden jaren werk voordat wiskundigen een moeilijk vermoeden kunnen bewijzen. In de twintigste eeuw hebben een aantal computerprogramma's zelfs stellingen bewezen die te moeilijk zijn voor onze beste wiskundigen. Worden wiskundige stellingen in de toekomst het alleenrecht van échte machines?



In 1997 versloeg Deep Blue, een supercomputer van IBM, toenmalig wereldkampioen Gary Kasparov in een schaaktoernooi. Eind 2006 werd Kasparovs opvolger Vladimir Kramnik in een toernooi verslagen door het schaakprogramma Deep Fritz 10. Ditmaal was er geen supercomputer meer nodig, maar een flink uit de kluiten gewassen bureaucomputer. In juli 2007 wonnen twee professionele pokerspelers maar nipt van een pokerprogramma. Het is nog maar een kwestie van tijd totdat de wereldkampioen poker verslagen wordt door een computer.



De nederlaag van Kasparov tegen Deep Blue bracht heel wat emoties los: mensen vonden dat computers schaak dood maakten. Anderen beweerden dat Deep Blue niet 'echt' schaak speelt, omdat de computer immers niets van schaak begrijpt: het is maar een massa rekenwerk. Ook de wiskundige bewijzen die door computerprogramma's geleverd werden, kregen te maken met zo'n negatieve reacties. Filosofen zeurden dat computerbewijzen geen échte wiskundige kennis geven en wiskundigen vonden dat deze bewijzen hen geen inzicht gaven in waarom de stelling juist geldt. Vooral dat laatste is problematisch: de computer zegt je wel dat de stelling waar is, maar je hebt er geen flauw idee van waarom, omdat het bewijs van de computer veel te lang en te ingewikkeld is.



Het eerste grote computerbewijs werd in 1976 afgewerkt door de Amerikaanse wiskundigen Kenneth Appel en Wolfgang Haken. Hun programma bewees de vierkleurenstelling. Deze stelling zegt dat het voor een willekeurige landkaart mogelijk is om de landen met hoogstens vier kleuren zó in te kleuren dat geen twee aangrenzende landen dezelfde kleur hebben. Met aangrenzend bedoelen we dat de landen een grens delen, dus landen die slechts in een punt aan elkaar liggen (zoals twee overliggende spieën van een gesneden taart) zijn niet aangrenzend. Met een land bedoelen we bovendien een samenhangend deel van de kaart, dus bijvoorbeeld niet de Verenigde Staten met Alaska erbij. Een student formuleerde in 1852 het vermoeden dat elke kaart op deze manier met vier kleuren in te kleuren is, waarna heel wat wiskundigen zich over het probleem bogen.



Het uiteindelijke bewijs van Appel en Haken bestond uit twee delen: het eerste deel beschreef de globale bewijsstrategie en een groot aantal regels om een verzameling van mogelijke delen van een kaart te construeren. Het tweede deel somde een zogenaamde 'onvermijdelijke verzameling' van delen van een kaart op: elke mogelijke kaart bevat minstens één deelkaart uit deze verzameling. De wiskundigen hadden ook een computerprogramma geschreven dat van elk van deze deelkaarten probeerde te bewijzen dat het niet kan voorkomen in een kaart waarvoor vijf kleuren nodig zijn. De rest van het bewijs bestond uit massa's berekeningen door de computer. Hieruit bleek dat inderdaad geen enkel van deze deelkaarten kan voorkomen in een kaart waarvoor vijf kleuren nodig zijn. En aangezien elke kaart minstens één van deze deelkaarten bevat, hadden ze zo bewezen dat elke kaart maximum vier kleuren nodig heeft om correct ingekleurd te worden.



De reacties op dit bewijs waren hevig. Zo kloegen veel wiskundigen dat de berekeningen van de computer veel te uitgebreid waren om te kunnen nakijken, zoals ze bij een klassiek bewijs gewoon waren. Daarom konden ze niet zeker zijn of het bewijs wel correct is. Anderen ontkenden zelfs dat het een bewijs was. Zo vergeleek de wiskundige Bonsall het accepteren van een computerbewijs met het accepteren van het woord van een andere wiskundige die zegt dat hij de stelling heeft bewezen, maar het bewijs niet geeft. Wiskundigen begrijpen het bewijs volgens hem niet, en hij noemt computerbewijzen dan ook 'quasi-bewijzen'. De wiskundige Paul Halmos ging zelfs verder: 'Het huidige bewijs [van de vierkleurenstelling] vertrouwt eigenlijk op een orakel, en ik zeg "weg met orakels!" Dit is geen wiskunde.'



Haken werd na zijn bewijs soms zelfs vijandig benaderd. Eén wiskundige probeerde te vermijden dat Haken contact kreeg met de studenten in zijn departement. Omdat het bewijs van de vierkleurenstelling was geleverd, zouden andere wiskundigen volgens hem niet meer proberen om een alternatief bewijs te vinden. Alle eer gaat immers naar het eerste bewijs. Maar omdat Haken het probleem op een 'ongepaste' manier had opgelost, aldus die collega, zou een beter bewijs er nooit komen. Haken vertelt hierover: 'We hadden iets heel ergs gedaan en zoiets mocht niet meer gebeuren, en daarom moest hij de onschuldige zielen van zijn studenten tegen ons beschermen.



'Gelukkig waren er ook nog nuchtere geesten, zoals de wiskundige Edwart Swart, die ook had geprobeerd om de vierkleurenstelling te bewijzen. Hij zag het belang van het computerbewijs in en begreep al die hysterie niet: 'Waarom zouden we wel bewijzen met potlood en papier aanvaarden, maar geen bewijzen met behulp van een computer?' Een bewijs dat gebruik maakt van computerberekeningen zag hij gewoon als een uitbreiding van hulpmiddelen als pen en papier.



Anno 2007 zijn er niet veel wiskundigen meer die echt twijfelen aan de correctheid van computerbewijzen. Dit komt enerzijds omdat wiskundigen meer en meer vertrouwd zijn met computers. Programma's als Mathematica en Maple om wiskundige berekeningen uit te voeren staan op de pc van veel wiskundigen. Anderzijds bestaan er ondertussen ook computerprogramma's die de correctheid van bewijzen in digitale vorm kunnen nagaan. Als het programma zo'n computerbewijs met succes nagekeken heeft, kunnen we er zeker van zijn dat het bewijs correct is, tenzij het programma zelf niet correct is. Maar dit programma is veel kleiner dan de meestal grote computerbewijzen, dus wiskundigen kunnen de correctheid van het programma nagaan.



Een probleem dat echter blijft, is dat computerbewijzen vaak niet inzichtelijk zijn. Het zijn vaak lange berekeningen die niemand in zijn geheel kan nakijken. Als je delen ervan nakijkt, zie je ook niet echt de ideeën die achter het bewijs zitten. Je verliest jezelf al vlug in het nakijken van een hoop details. Dat is dan ook één van de redenen waarom veel wiskundigen wel computerprogramma's zoals Mathematica gebruiken om berekeningen uit te voeren, maar slechts weinig wiskundigen computerprogramma's gebruiken om delen van een bewijs te construeren.



Uit deze studie blijkt dat het idee van wiskundigen als machines om koffie in stellingen om te zetten niet zo vruchtbaar is. Voor wiskundigen telt immers meer dan enkel het resultaat. Wat er in het hoofd van een wiskundige gebeurt is even belangrijk als de koffie die erin gaat en de stelling die eruit gaat. Hetzelfde geldt voor computers: niet enkel de bits die je erin giet en het antwoord 'de stelling klopt' zijn belangrijk, ook de manier waarop de computer de stelling bewezen heeft. Zolang de computer dit niet zoals een echte wiskundige doet, kan hij nooit de wiskundige vervangen.Koen Vervloesem

Bibliografie

Literatuurlijst



[Aberdein2006] Andrew Aberdein, ‘The informal logic of mathematical proof’, in Reuben

Hersh (ed.), 18 unconventional essays on the nature of mathematics (2006),

Springer, New York, pp. 56-70



[Adams1999] Andrew Adams, Hanne Gottliebsen, Steve Linton en Ursula Martin,

‘Automated theorem proving in support of computer algebra: symbolic definite

integration as a case study’, Proceedings of the 1999 international symposium on

Symbolic and algebraic computation (1999), pp. 253-260



[Adams2001] Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula

Martin en Sam Owre, ‘Computer Algebra meets Automated Theorem Proving:

Integrating Maple and PVS’, Lecture Notes in Computer Science, 14th International

Conference on Theorem Proving in Higher Order Logics, Vol. 2152 (2001),

pp. 27-42



[Adleman1994] Leonard M. Adleman, ‘Molecular computation of solutions to combinatorial

problems’, Science, Vol. 266, No. 5187 (1994), pp. 1021-1024



[Aigner2004] Martin Aigner en Günter Ziegler, Proofs from THE BOOK, Third Edition

(2004), Springer, pp. 239



[Albers1981] Donald J. Albers, ‘Polite applause for a proof of one of the great conjectures

of mathematics: what is a proof today?’, The Two-Year College Mathematics

Journal, Vol. 12, No. 2 (1981), pp. 82



[Appel1977] Kenneth Appel en Wolfgang Haken, ‘Every planar map is four-colorable’,

Part I. Discharging, Illinois Journal of Mathematics, Vol. 21 (1977), pp. 429-490



[Appel1977b] Kenneth Appel, Wolfgang Haken en John Koch, ‘Every planar map is

four-colorable’, Part II. Reducibility, Illinois Journal of Mathematics, Vol. 21

(1977), pp. 491-567



[Appel1977c] Kenneth Appel en Wolfgang Haken, ‘The solution of the four-color map

problem’, Scientific American, Vol. 237, No. 4 (1977), pp. 108-121



[Appel1978] Kenneth Appel en Wolfgang Haken, ‘The four-color problem’, in Lynn

Arthur Steen (ed.), Mathematics today: twelve informal essays (1978), Springer-

Verlag, New York, pp. 153-180, in [Jacquette2001], pp. 193-208



[Aschbacher2004] Michael Aschbacher, ‘The status of the classification of the finite simple

groups’, Notices of the American Mathematical Society, Vol. 51, No. 7

(2004), pp. 736-740



[Aschbacher2005] Michael Aschbacher, ‘Highly complex proofs and implications of

such proofs’, Philosophical Transactions of the Royal Society A, Vol. 363 (2005),

pp. 2401-2406



[Avigad2006] Jeremy Avigad, ‘Mathematical method and proof’, Synthese, Vol. 153, No.

1 (2006), pp. 105-159



[Avigad2007] Jeremy Avigad, ‘Understanding proofs’, in [Mancosu2007]



[Avigad2007b] Jeremy Avigad, ‘Computers in mathematical inquiry’, in [Mancosu2007]



[Azzouni2004] Jody Azzouni, ‘The derivation-indicator view of mathematical practice’,

Philosophia Mathematica, Vol. 12, No. 2 (2004), pp. 81-106



[Azzouni2005] Jody Azzouni, ‘Is there still a sense in which mathematics can have foundations?’,

in Giandomenico Sica (ed.), Essays on the Foundations of Mathematics

and Logic., Advanced Studies in Mathematics and Logic, 1 (2005), Polimetrica,

Monza, pp. 9-47



[Barendregt2001] Henk Barendregt en Arjeh M. Cohen, ‘Electronic communication of

mathematics and the interaction of computer algebra systems and proof

assistants’, Journal of Symbolic Computation, Vol. 32 (2001), pp. 3-22



[Barendregt2002] Henk Barendregt en Erik Barendsen, ‘Autarkic computations in formal

proofs’, Journal of Automated Reasoning, Vol. 28, No. 3 (2002), pp. 321-336



[Barendregt2005] Henk Barendregt en Freek Wiedijk, ‘The challenge of computer mathematics’,

Philosophical Transactions of the Royal Society, Vol. 363 (2005), pp.

2351-2375



[Bassler2006] O. Bradley Bassler, ‘The surveyability of mathematical proof: a historical

perspective’, Synthese, Vol. 148 (2006), pp. 99-133



[Bauer2006] Gertrud Josefine Bauer, Formalizing plane graph theory - towards a formalized

proof of the Kepler conjecture, Thesis voor de graad van doctor in de natuurwetenschappen,

Fakultät für Informatik, Technische Universiteit München

(2006), pp. 188



[Bauer2006b] Gertrud Bauer en Tobias Nipkow, ‘Towards a verified enumeration of all

tame plane graphs’, in Thierry Coquand, Henri Lombardi, Marie-Françoise Roy,

Mathematics, Algorithms, Proofs (2006), Internationales Begegnungs- und Forschungszentrum

fuer Informatik, Schloss Dagstuhl



[Beeson1998] Michael Beeson, ‘Automatic derivation of epsilon-delta proofs of continuity’,

Lecture Notes in Artificial Intelligence, Artificial Intelligence and Symbolic

Computation, Vol. 1476 (1998), pp. 67-83



[Beeson2001] Michael Beeson, ‘Automatic derivation of the irrationality of e’, Journal

of Symbolic Computation, Vol. 32, No. 4 (2001), pp. 333-349



[Beeson2003] Michael Beeson, ‘The mechanization of mathematics’, in C. Teuscher

(ed.), Alan Turing: Life and Legacy of a Great Thinker (2003), Springer-Verlag,

pp. 77-134



[Belinfante1999] Johan G. Belinfante, ‘On computer-assisted proofs in ordinal number

theory’, Journal of Automated Reasoning, Vol. 22 (1999), pp. 341-378



[Benacerraf1965] Paul Benacerraf, ‘What numbers could not be’, The Philosophical Review,

Vol. 74, No. 1 (1965), pp. 47-73



[Benacerraf1973] Paul Benacerraf, ‘Mathematical truth’, The Journal of Philosophy, Vol.

70, No. 19 (1973), pp. 661-679



[Benzmüller2001] Christoph Benzmüller, Andreas Meier, Erica Melis, Martin Pollet,

Jörg Siekmann en Volker Sorge, ‘Proof planning: a fresh start?’, Workshop on

Future Directions in Automated Reasoning (W1) on IJCAR 2001 (2001), pp.

25-37



[Berkovich2002] Alexander Berkovich en Axel Riese, ‘A computer proof of a polynomial

identity implying a partition theorem of Göllnitz’, Advances in Applied Mathematics,

Vol. 28 (2002), pp. 1-16



[Bondecka2004] Izabela Bondecka-Krzykowska, ‘The four-color theorem and its consequences

for the philosophy of mathematics’, Annales UMCS Informatica AI, Vol.

2 (2004), pp. 5-14



[Bonsall1982] F. F. Bonsall, ‘A down-to-earth view of mathematics’, The American Mathematical

Monthly, Vol. 89, No. 1 (1982), pp. 8-15



[Bose1959] Raj Chandra Bose en Sharadchandra Shankar Shrikhande, ‘On the falsity of

Euler's conjecture about the non-existence of two orthogonal Latin squares of order

4t + 2’, Proceedings of the National Academy of Sciences, Vol. 45 (1959), pp.

734-737



[Bose1960] Raj Chandra Bose en Sharadchandra Shankar Shrikhande, ‘On the construction

of sets of mutually orthogonal Latin squares and the falsity of a conjecture of

Euler’, Transactions of the American Mathematical Society, Vol. 95, No. 2

(1960), pp. 191-209



[Bundy1988] Alan Bundy, ‘The use of explicit plans to guide inductive proofs’, Lecture

Notes in Computer Science, Ninth Conference on Automated Deduction, Vol. 203

(1988), pp. 111-120



[Bundy1991] Alan Bundy, Frank van Harmelen, Jane Hesketh en Alan Smaill,

‘Experiments with proof plans for induction’, Journal of Automated Reasoning,

Vol. 7, No. 3 (1991), pp. 303-324



[Bundy1991b] Alan Bundy, ‘A science of reasoning’, in Jean-Louis Lassez, Gordon Plotkin,

Computational Logic: Essays in Honor of Alan Robinson (1991), pp.

178-198, MIT Press



[Bundy1993] Alan Bundy, Andrew Stevens, Frank van Harmelen, Andrew Ireland en

Alan Smaill, ‘Rippling: A heuristic for guiding inductive proofs’, Artificial Intelligence,

Vol. 62, No. 2 (1993), pp. 185-253



[Bundy1998] Alan Bundy, ‘Proof planning’, Proceedings of the 3rd International Conference

on AI Planning Systems (1998), pp. 261-267



[Bundy1999] Alan Bundy, Simon Colton en Toby Walsh, ‘HR - A system for machine

discovery in finite algebras’, Proceedings of the Machine Discovery Workshop

ECAI99 (1999)



[Bundy1999b] Alan Bundy en Julian Richardson, ‘Proofs about lists using ellipsis’, Lecture

Notes in Artificial Intelligence, Proceedings of the 6th International Conference,

Logic for Programming and Automated Reasoning, Vol. 1705 (1999), pp.

1-12



[Bundy1999c] Alan Bundy, ‘A survey of automated deduction’, Lecture Notes in Computer

Science, Artificial Intelligence Today: Recent Trends and Developments,

Vol. 1600 (1999), pp. 153-174



[Bundy2001] Alan Bundy, ‘The automation of proof by mathematical induction’, in [Robinson2001]



[Bundy2005] Alan Bundy, Mateja Jamnik en Andrew Fugard, ‘What is a proof?’, Philosophical

Transactions of the Royal Society, Vol. 363 (2005), pp. 2377-2391



[Bundy2006] Alan Bundy, ‘The Boole Lecture’, A very mathematical dilemma, The

Computer Journal, Vol. 49, No. 4 (2006), pp. 480-486



[Burge1993] Tyler Burge, ‘Content preservation’, The Philosophical Review, Vol. 102,

No. 4 (1993), pp. 457-488



[Burge1998] Tyler Burge, ‘Computer proof, apriori knowledge, and other minds’, Philosophical

Perspectives, Vol. 12 (Language, Mind, and Ontology) (1998), pp. 1-37



[Burris1996] Stanley Burris, An anthropomorphized version of McCune's machine proof

that Robbins algebras are Boolean algebras (1996), Ongepubliceerd manuscript

(http://www.cs.unm.edu/~mccune/old-ftp/www-misc/burris-robbins-prf.ps.gz)



[Cairns1954] Stewart Scott Cairns, ‘Computational attacks on discrete problems’, The

American Mathematical Monthly, Vol. 61, No. 7 (1954), pp. 29-31



[Calude2001] Andreea S. Calude, ‘The journey of the four colour theorem through time’,

The New Zealand Mathematics Magazine, Vol. 38, No. 3 (2001), pp. 27-35



[Caprotti2001] Olga Caprotti en Martijn Oostdijk, ‘Formal and efficient primality proofs

by use of computer algebra oracles’, Journal of Symbolic Computation, Vol. 32

(2001), pp. 55-70



[Casselman2000] Bill Casselman, ‘Pictures and proofs’, Notices of the American Mathe-

matical Society, Vol. 47, No. 10 (2000), pp. 1257-1266



[Cayley1879] Arthur Cayley, ‘On the colouring of maps’, Proceedings of the Royal Geographical

Society and Monthly Record of Geography, Vol. 1, No. 4 (1879), pp.

259-261



[Cerutti1969] Elsie Cerutti en Philip J. Davis, ‘Formac meets Pappus: some observations

on elementary analytic geometry by computer’, The American Mathematical

Monthly, Vol. 76, No. 8 (1969), pp. 895-905



[Chaitin1974] Gregory J. Chaitin, ‘Information-theoretic computational complexity’,

IEEE Transactions on Information Theory, Vol. IT-20, No. 1 (1974), pp. 10-15,

in [Tymoczko1998]



[Chaitin1975] Gregory J. Chaitin, ‘Randomness and mathematical proof’, Scientific American,

Vol. 232, No. 5 (1975), pp. 47-52



[Chaitin1978] Gregory J. Chaitin en Jacob T. Schwartz, ‘A note on Monte Carlo primality

tests and algorithmic information theory’, Communications on Pure and Applied

Mathematics, Vol. 31 (1978), pp. 521-527



[Chaitin1982] Gregory J. Chaitin, ‘Gödel's theorem and information’, International

Journal of Theoretical Physics, Vol. 22 (1982), pp. 941-954, in [Tymoczko1998]



[Chaitin2002] Gregory J. Chaitin, ‘Computers, paradoxes and the foundations of mathematics’,

American Scientist, Vol. 90 (2002), pp. 164-171



[Chaitin2004] Gregory Chaitin, Irreducible complexity in pure mathematics (2004),

http://arxiv.org/abs/math.HO/0411091



[Chang2004] Kenneth Chang, ‘In math, computers don't lie. Or do they?’, The New York

Times (2004)



[Colton1999] Simon Colton, Alan Bundy en Toby Walsh, ‘Automatic concept formation

in pure mathematics’, Proceedings of the Sixteenth International Joint Conference

on Artificial Intelligence (1999), pp. 786-793



[Colton1999b] Simon Colton, ‘Refactorable numbers - a machine invention’, Journal of

Integer Sequences, Vol. 2 (1999), article 99.1.2



[Colton2000] Simon Colton, Alan Bundy en Toby Walsh, ‘On the notion of interestingness

in automated mathematical discovery’, International Journal of Human

Computer Studies, Vol. 53, No. 3 (2000), pp. 351-375



[Conway1999] John Horton Conway, Chaim Goodman-Strauss en Neil James Alexander

Sloane, ‘Recent progress in sphere packing’, in Barry Mazur, W. Schmid, S. T.

Yau, D. Jerison, I. Singer, D. Stroock, Current Developments in Mathematics

(1999), International Press, Somerville, MA, pp. 37-76



[Coolsaet2005] Kris Coolsaet en Jan Degraer, ‘A computer-assisted proof of the unique-

ness of the Perkel graph’, Designs, Codes and Cryptography, Vol. 34 (2005), pp.

155-171



[Corfield2003] David Corfield, Towards a philosophy of real mathematics (2003), Cambridge

University Press, pp. 287



[Crilly2005] Tony Crilly, ‘Arthur Cayley FRS and the four-colour map problem’, Notes

& Records of the Royal Society, Vol. 59 (2005), pp. 285-304



[Dahn1997] Bernd Dahn, An explanation of EQP/Otter's proof of Winker's second condition

for Robbins algebras (1997), Ongepubliceerd manuscript



[Davies2005] Brian Davies, ‘Whither Mathematics?’, Notices of the American Mathematical

Society, Vol. 52, No. 11 (2005), pp. 1350-1356



[Davis1972] Philip J. Davis, ‘Fidelity in mathematical discourse: is one and one really

two?’, The American Mathematical Monthly, Vol. 79, No. 3 (1972), pp. 252-263,

in [Tymoczko1998], pp. 163-176



[Davis2001] Martin Davis, ‘The early history of automated deduction’, in [Robinson2001],

pp. 3-15



[Dawson2006] John W. Dawson, Jr, ‘Why do mathematicians re-prove theorems?’, Philosophia

Mathematica, Vol. 14, No. 3 (2006), pp. 269-286



[DeMillo1979] Richard De Millo, Richard Lipton en Alan Perlis, ‘Social processes and

proofs of theorems and programs’, Communications of the American Mathematical

Society, Vol. 22, No. 5 (1979), pp. 271-280, in [Tymoczko1998], pp. 267-286



[Detlefsen1980] Michael Detlefsen en Mark Luker, ‘The four-color theorem and mathematical

proof’, The Journal of Philosophy, Vol. 77, No. 12 (1980), pp. 803-820



[Dove2002] Ian Dove, ‘Can pictures prove?’, Logique & Analyse, Vol. 179-180 (2002),

pp. 309-340



[Ernst2002] Bruno Ernst (ed.), De interessantste bewijzen voor de stelling van Pythagoras

(2002), Epsilon Uitgaven, Utrecht, pp. 95



[Euler1738] Leonhard Euler, ‘Observationes de theoremate quodam Fermatiano aliisque

ad numeros primos spectantibus’, Commentarii academiae scientiarum imperialis

Petropolitanae, Vol. 6 (1738), pp. 103-107, Vertaald in het Engels op

http://arxiv.org/PS_cache/math/pdf/0501/0501118.pdf



[Euler1750] Leonhard Euler, ‘Theoremata circa divisores numerorum’, Novi Commentarii

academiae scientiarum Petropolitanae, Vol. 1 (1750), pp. 20-48, Vertaald in

het Engels op http://www.cs.utexas.edu/users/wzhao/e134.pdf



[Fallis1996] Don Fallis, ‘Mathematical proof and the reliability of DNA evidence’, The

American Mathematical Monthly, Vol. 103, No. 6 (1996), pp. 491-497



[Fallis1997] Don Fallis, ‘The epistemic status of probabilistic proof’, The Journal of Phi-

losophy, Vol. 94, No. 4 (1997), pp. 165-186



[Fallis2002] Don Fallis, ‘What do mathematicians want? Probabilistic proofs and the

epistemic goals of mathematicians’, Logique & Analyse, Vol. 179-180 (2002), pp.

373-388



[Fallis2003] Don Fallis, ‘Intentional gaps in mathematical proofs’, Synthese, Vol. 134

(2003), pp. 45-69



[Ferguson2006] Samuel P. Ferguson, ‘Sphere packings’, V. Pentahedral prisms, Discrete

and Computational Geometry, Vol. 36, No. 1 (2006), pp. 167-204



[Fikes1971] Richard Fikes en Nils Nilsson, ‘STRIPS: A new approach to the application

of theorem proving to problem solving’, Artificial Intelligence, Vol. 2 (1971), pp.

189-208



[Fitelson1998] Branden Fitelson, ‘Using Mathematica to Understand the Computer Proof

of the Robbins Conjecture’, Mathematica in Education and Research, Vol. 7, No.

1 (1998), pp. 17-26



[Franklin1922] Philip Franklin, ‘The four color problem’, American Journal of Mathematics,

Vol. 44, No. 3 (1922), pp. 225-236



[Gabai2003] David Gabai, G. Robert Meyerhoff en Nathaniel Thurston, ‘Homotopy hyperbolic

3-manifolds are hyperbolic’, Annals of Mathematics, Vol. 157, No. 2

(2003), pp. 335-431



[Galda1981] Klaus Galda, ‘An informal history of formal proofs: from vigor to rigor?’,

The Two-Year College Mathematics Journal, Vol. 12, No. 2 (1981), pp. 126-140



[Gödel1931] Kurt Gödel, ‘Über formal unentscheidbare Sätze der Principia Mathematica

und verwandter Systeme, I’, Monatshefte für Mathematik und Physik, Vol. 38

(1931), pp. 173-198



[Gonthier2004] Georges Gonthier, A computer-checked proof of the four colour theorem

(2004), Ongepubliceerd manuscript

(http://research.microsoft.com/~gonthier/4colproof.pdf)



[Gorissen2007] Marcel J.G. Gorissen, Generating finite projective planes from nonparatopic

Latin squares, Thesis voor de graad van Master of Science in Mathematics,

Radboud Universiteit Nijmegen (2007),

http://www.math.kun.nl/~bosma/students/gorissen/gorissenmscthesis.pdf



[Hales2000] Thomas C. Hales, ‘Cannonballs and honeycombs’, Notices of the American

Mathematical Society, Vol. 47, No. 4 (2000), pp. 440-449



[Hales2001] Thomas C. Hales, ‘The honeycomb conjecture’, Discrete and Computational

Geometry, Vol. 25 (2001), pp. 1-22



[Hales2002] Thomas C. Hales, Sphere packings in 3 dimensions (2002), Arbeitstagung

lezing in Bonn, 14 juni 2001

(http://www.math.pitt.edu/~thales/PUBLICATIONS/spherepacking3.pdf)



[Hales2002b] Thomas C. Hales, ‘A computer verification of the Kepler conjecture’, Proceedings

of the International Congress of Mathematicians, Vol. 3 (2002), pp.

795-804



[Hales2003] Thomas C. Hales, ‘Some algorithms arising in the proof of the Kepler conjecture’,

Algorithms and Combinatorics, Vol. 25 (2003), pp. 489-508



[Hales2005] Thomas C. Hales, ‘A proof of the Kepler conjecture’, Annals of Mathematics,

Vol. 162, No. 3 (2005), pp. 1065-1185



[Hales2006] Thomas C. Hales, ‘Historical overview of the Kepler conjecture’, Discrete

and Computational Geometry, Vol. 36, No. 1 (2006), pp. 5-20



[Hales2006b] Thomas C. Hales en Samuel P. Ferguson, ‘A formulation of the Kepler

conjecture’, Discrete and Computational Geometry, Vol. 36, No. 1 (2006), pp.

21-69



[Hales2006c] Thomas C. Hales, ‘Sphere packing’, III. Extremal cases, Discrete and

Computational Geometry, Vol. 36, No. 1 (2006), pp. 71-110



[Hales2006d] Thomas C. Hales, ‘Sphere packing’, IV. Detailed bounds, Discrete and

Computational Geometry, Vol. 36, No. 1 (2006), pp. 111-166



[Hales2006e] Thomas C. Hales, ‘Sphere packings’, VI. Tame graphs and linear

programs, Discrete and Computational Geometry, Vol. 36, No. 1 (2006), pp.

205-265



[Hales2006f] Thomas C. Hales, ‘Introduction to the Flyspeck project’, in Thierry Coquand,

Henri Lombardi, Marie-Françoise Roy, Mathematics, Algorithms,

Proofs (2006), Internationales Begegnungs- und Forschungszentrum fuer Informatik,

Schloss Dagstuhl



[Hall1955] Marshall Hall Jr., ‘Finite projective planes’, The American Mathematical

Monthly, Vol. 62, No. 7 (1955), pp. 18-24



[Halmos1990] Paul Richard Halmos, ‘Has progress in mathematics slowed down?’, The

American Mathematical Monthly, Vol. 97, No. 7 (1990), pp. 561-588



[Hardy1929] Godfrey Harold Hardy, ‘Mathematical proof’, Mind, Vol. 38, No. 149

(1929), pp. 1-25, in [Jacquette2001], pp. 173-186



[Hass1995] Joel Hass, Michael Hutchings en Roger Schlafly, ‘The double bubble conjecture’,

Electronic Research Announcements of the American Mathematical Society,

Vol. 1, No. 3 (1995), pp. 98-102



[Hass2000] Joel Hass en Roger Schlafly, ‘Double bubbles minimize’, Annals of Mathematics,

Vol. 151, No. 2 (2000), pp. 459-515



[Heawood1890] Percy John Heawood, ‘Map colouring theorem’, Quarterly Journal of

Pure and Applied Mathematics, Vol. 24 (1890), pp. 332-338



[Hersh1993] Reuben Hersh, ‘Proving is convincing and explaining’, Educational Studies

in Mathematics, Vol. 24, No. 4 (1993), pp. 389-399



[Hersh1997] Reuben Hersh, ‘Prove –once more and again’, Philosophia Mathematica,

Vol. 5, No. 2 (1997), pp. 153-165



[Hlinený2002] Petr Hlinený, ‘On the excluded minors for matroids of branch-width

three’, The Electronic Journal of Combinatorics, Vol. 9, No. 1 (2002),

http://www.combinatorics.org/Volume_9/Abstracts/v9i1r32.html



[Horsten2001] Leon Horsten, ‘Platonistic formalism’, Erkenntnis, Vol. 54, No. 2 (2001),

pp. 173-194



[Horsten2004] Leon Horsten (ed.), Eindig, oneindig, meer dan oneindig, Grondslagen

van de wiskundige wetenschappen (2004), Epsilon Uitgaven, Utrecht, pp. 203



[Hsiang1993] Wu-Yi Hsiang, ‘On the sphere packing problem and the proof of Kepler's

conjecture’, International Journal of Mathematics, Vol. 4, No. 5 (1993), pp.

739-831



[Huang2002] Tony Huang, Automated deduction in ring theory, Master's Writing Project,

Department of Computer Science, San Jose State University (2002)



[Huntington1933] Edward Vermilye Huntington, ‘New sets of independent postulates for

the algebra of logic, with special reference to Whitehead and Russell's Principia

Mathematica’, Transactions of the American Mathematical Society, Vol. 35, No.

1 (1933), pp. 274-304



[Huntington1933b] Edward Vermilye Huntington, ‘Boolean algebra. A correction’,

Transactions of the American Mathematical Society, Vol. 35, No. 2 (1933), pp.

557-558



[Jacquette2001] Dale Jacquette (ed.), Philosophy of mathematics: an anthology (2001),

Blackwell Publishers, pp. 428



[Jones1998] Vaughan Frederick Randal Jones, ‘A credo of sorts’, in H. G. Dales, Gianluigi

Oliveri, Truth in mathematics (1998), Oxford University Press, pp. 203-214



[Katz1995] Jerrold J. Katz, ‘What mathematical knowledge could be’, Mind, Vol. 104,

No. 415 (1995), pp. 491-522



[Kauffman1990] Louis H. Kauffman, ‘Robbins algebra’, Proceedings of the Twentieth

International Symposium on Multiple-Valued Logic (1990), pp. 54-60



[Kauffman2001] Louis H. Kauffman, ‘The Robbins problem: computer proofs and human

proofs’, Kybernetes, Vol. 30, No. 5/6 (2001), pp. 726-751



[Kempe1879] Alfred Bray Kempe, ‘On the geographical problem of the four colours’,

American Journal of Mathematics, Vol. 2, No. 3 (1879), pp. 193-200



[Kerber1998] Manfred Kerber, Michael Kohlhase en Volker Sorge, ‘Integrating computer

algebra into proof planning’, Journal of Automated Reasoning, Vol. 21, No. 3

(1998), pp. 327-355



[Kerber2002] Manfred Kerber en Martin Pollet, ‘On the design of mathematical concepts’,

Lecture Notes in Computer Science, Proceedings of the 15th Australian

Joint Conference on Artificial Intelligence: Advances in Artificial Intelligence,

Vol. 2557 (2002)



[Kleiner1991] Israel Kleiner, ‘Rigor and proof in mathematics: a historical perspective’,

Mathematics Magazine, Vol. 64, No. 5 (1991), pp. 291-314



[Kolata1996] Gina Kolata, ‘Computer math proof shows reasoning power’, The New

York Times (1996), http://www.nytimes.com/library/cyber/week/1210math.html



[Krakowski1980] Israel Krakowski, ‘The four color problem reconsidered’, Philosophical

Studies, Vol. 38 (1980), pp. 91-96



[Krízek2001] Michal Krízek, Florian Luca en Lawrence Somer, 17 Lectures on Fermat

numbers, From number theory to geometry (2001), Springer, New York, pp. 257



[Lam1989] Clement W.H. Lam, L. Thiel en S. Swiercz, ‘The non-existence of finite projective

planes of order 10’, Canadian Journal of Mathematics, Vol. XLI (1989),

pp. 1117-1123



[Lam1991] Clement W.H. Lam, ‘The search for a finite projective plane of order 10’,

The American Mathematical Monthly, Vol. 98, No. 4 (1991), pp. 305-318



[Lamport1995] Leslie Lamport, ‘How to write a proof’, The American Mathematical

Monthly, Vol. 102, No. 7 (1995), pp. 600-608



[Lehmer1962] Derrick Henry Lehmer, Emma Lehmer, William H. Mills en John L.

Selfridge, ‘Machine proof of a theorem on cubic residues’, Mathematics of computation,

Vol. 16, No. 80 (1962), pp. 407-415



[Levin1981] Margarita Levin, ‘On Tymoczko's argument for mathematical empiricism’,

Philosophical Studies, Vol. 39 (1981), pp. 79-86



[MacLane1997] Saunders Mac Lane, ‘Despite physicists, proof is essential in mathematics’,

Synthese, Vol. 111, No. 2 (1997), pp. 147-154



[MacKay1985] Robert Sinclair MacKay en I. C. Percival, ‘Converse KAM: theory and

practice’, Communications in mathematical physics, Vol. 98, No. 4 (1985), pp.

469-512



[MacKenzie1999] Donald MacKenzie, ‘Slaying the Kraken: the sociohistory of a mathematical

proof’, Social Studies of Science, Vol. 29, No. 1 (1999), pp. 7-60



[Mackenzie2005] Dana Mackenzie, ‘What in the name of Euclid is going on here?’, Science,

Vol. 307, No. 5714 (2005), pp. 1402-1403



[MacWilliams1973] Florence Jessie MacWilliams, Neil J.A. Sloane en John Griggs

Thompson, ‘On the existence of a projective plane of order 10’, Journal of Combinatorial

Theory, Vol. 14, No. 1 (1973), pp. 66-78



[Maddy1997] Penelope Maddy (ed.), Naturalism in Mathematics (1997), Clarendon

Press, Oxford



[Mallows1974] Colin L. Mallows en Neil J.A. Sloane, ‘Weight enumerators of selforthogonal

codes’, Discrete Mathematics, Vol. 9 (1974), pp. 391-400



[Mancosu1991] Paolo Mancosu, ‘On the status of proofs by contradiction in the seventeenth

century’, Synthese, Vol. 88 (1991), pp. 15-41



[Mancosu2001] Paolo Mancosu, ‘Mathematical explanation: problems and prospects’,

Topoi, Vol. 20 (2001), pp. 97-117



[Mancosu2007] Paolo Mancosu (ed.), The Philosophy of Mathematical Practice (2007),

Oxford University Press, Oxford



[Mandelbrojt1952] Szolem Mandelbrojt, ‘Pourquoi je fais des mathématiques’, Revue de

métaphysique et de morale, Vol. 57, No. 4 (1952), pp. 442-429, Cahiers du séminaire

d'histoire des mathématiques, Vol. 6 (1985), pp. 47-54



[Manin1981] Yuri I. Manin, ‘A digression on proof’, The Two-Year College Mathematics

Journal, Vol. 12, No. 2 (1981), pp. 104-107



[Mann2003] Allen Lawrence Mann, A case study in automated theorem proving: Otter

and EQP, Thesis submitted to the Faculty of the Graduate School of the University

of Colorado for the degree of Master of Arts in Mathematics (2003),

http://math.colorado.edu/~almann/MA/thesis.pdf



[Martin1999] Ursula Martin, ‘Computers, reasoning and mathematical practice’, Computational

Logic, Vol. 165 (1999), pp. 301-346



[May1965] Kenneth O. May, ‘The origin of the four-color conjecture’, Isis, Vol. 56, No.

3 (1965), pp. 346-348



[Mayer1982] Jean Mayer, ‘Le théorème des quatre couleurs: notice historique et aperçu

technique’, Cahiers du séminaire d'histoire des mathématiques, Vol. 3 (1982), pp.

43-62



[McCasland2006] Roy L. McCasland, Alan Bundy en Patrick F. Smith, ‘Ascertaining

mathematical theorems’, Electronic Notes in Theoretical Computer Science, Proceedings

of the 12th Symposium on the Integration of Symbolic Computation and

Mechanized Reasoning (Calculemus 2005), Vol. 151 (2006), pp. 21-38



[McCune1997] William McCune, ‘Solution of the Robbins problem’, Journal of Auto-

mated Reasoning, Vol. 19, No. 3 (1997), pp. 263-276



[McCune1997b] William McCune, ‘Well-behaved search and the Robbins problem’,

Proceedings of the 8th International Conference on Rewriting Techniques and

Applications (1997), pp. 1-7



[McCune2002] William McCune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew

Feist en Larry Wos, ‘ Short single axioms for Boolean algebra’, Journal of

automated reasoning, Vol. 29, No. 1 (2002), pp. 1-16



[Melis1996] Erica Melis en Alan Bundy, ‘Planning and proof planning’, S. Biundo (ed.),

ECAI-96 Workshop on Cross-Fertilization in Planning (1996), pp. 37-40



[Miller1975] Gary L. Miller, ‘Riemann's hypothesis and tests for primality’, Proceedings

of seventh annual ACM symposium on Theory of computing (1975), pp. 234-239



[Mitchem1981] John Mitchem, ‘On the history and solution of the four-color map problem’,

The Two-Year College Mathematics Journal, Vol. 12, No. 2 (1981), pp.

108-116



[Monroy1994] Raul Monroy, Alan Bundy en Andrew Ireland, ‘Proof plans for the correction

of false conjectures’, Lecture Notes in Computer Science, Proceedings of

the Fifth International Conference on Logic Programming and Automated Reasoning,

Vol. 822 (1994), pp. 54-68



[Mumford1967] David Mumford, ‘On the equations defining abelian varieties. III’, Inventiones

Mathematicae, Vol. 3, No. 3 (1967), pp. 215-244



[Muñoz2006] Vicente Muñoz en Ulf Persson, ‘Interviews with three Fields medallists’,

Newsletter of the European Mathematical Society, No. 62 (2006), pp. 32-36



[Nipkow2006] Tobias Nipkow, Gertrud Bauer en Paula Schultz, ‘Flyspeck I: tame

graphs’, in U. Furbach, N. Shankar, Automated Reasoning (2006), Springer, pp.

21-35



[Norwood1982] F. H. Norwood, ‘Long proofs’, The American Mathematical Monthly,

Vol. 89, No. 2 (1982), pp. 110-112



[Obua2006] Steven Obua, ‘Proving bounds for real linear programs in Isabelle/HOL’, in

Thierry Coquand, Henri Lombardi, Marie-Françoise Roy, Mathematics, Algorithms,

Proofs (2006), Internationales Begegnungs- und Forschungszentrum fuer

Informatik, Schloss Dagstuhl



[Owings1973] James C. Owings, Jr, ‘Diagonalization and the recursion theorem’, Notre

Dame Journal of Formal Logic, Vol. 14, No. 1 (1973), pp. 95-99



[Pagin1994] Peter Pagin, ‘Knowledge of proofs’, Topoi, Vol. 13 (1994), pp. 93-100, in

[Jacquette2001], pp. 209-217



[Parker1959] E. T. Parker, ‘Orthogonal Latin squares’, Proceedings of the National Aca-

demy of Sciences, Vol. 45 (1959), pp. 859-862



[Parker1959b] E. T. Parker, ‘Construction of some sets of mutually orthogonal Latin

squares’, Proceedings of the American Mathematical Society, Vol. 10, No. 6

(1959), pp. 946-949



[Pastre1999] Dominique Pastre, Can and must a machine prove theorems as humans do

?, Analysis of some automated proofs by the MUSCADET system (1999), Intern

rapport (http://www.math-info.univ-paris5.fr/~pastre/CanAndMust.pdf)



[Paule2003] Peter Paule en Carsten Schneider, ‘Computer proofs of a new family of harmonic

number identities’, Advances in Applied Mathematics, Vol. 31 (2003), pp.

359-378



[Peterson1997] Ivars Peterson, ‘Computers and proof: applying automated reasoning to

prove mathematical theorems’, Science News, Vol. 151, No. 12 (1997), pp. 178



[Petkovsek1996] Marko Petkovsek, Herbert Wilf en Doron Zeilberger, A = B (1996), A

K Peters, pp. 212



[Rabin1976] Michael O. Rabin, ‘Probabilistic algorithms’, in J. F. Traub (ed.), Algorithms

and complexity - New directions and recent results (1976), Academic Press, New York, pp. 21-39



[Rabin1980] Michael O. Rabin, ‘Probabilistic algorithm for testing primality’, Journal of

Number Theory, Vol. 12, No. 1 (1980), pp. 128-138



[Rav1999] Yehuda Rav, ‘Why do we prove theorems?’, Philosophia Mathematica, Vol.

7, No. 1 (1999), pp. 5-41



[Renz1981] Peter Renz, ‘Mathematical proof: what it is and what it ought to be’, The

Two-Year College Mathematics Journal, Vol. 12, No. 2 (1981), pp. 83-103



[Resnik1981] Michael D. Resnik, ‘Mathematics as a science of patterns: ontology and reference’,

Noûs, Vol. 15, No. 4 (Special Issue on Philosophy of Mathematics)

(1981), pp. 529-550



[Resnik1982] Michael D. Resnik, ‘Mathematics as a science of patterns: epistemology’,

Noûs, Vol. 16, No. 1 (1982), pp. 95-105



[Resnik1987] Michael D. Resnik en David Kushner, ‘Explanation, independence and realism

in mathematics’, The British Journal for the Philosophy of Science, Vol. 38,

No. 2 (1987), pp. 141-158



[Resnik1992] Michael D. Resnik, ‘Proof as a source of truth’, in Michael Detlefsen (ed.),

Proof and Knowledge in Mathematics (1992), Routledge, pp. 6-32, in [Tymoczko1998],

pp. 317-336



[Richardson1999] Julian Richardson en Alan Bundy, ‘Proof planning methods as schemas’,

Journal of Symbolic Computation, Vol. 11 (1999)



[Riese2003] Axel Riese, ‘qMultiSum - A package for proving q-hypergeometric multiple

summation identities’, Journal of Symbolic Computation, Vol. 35 (2003), pp.

349-376



[Robertson1996] Neil Robertson, Daniel P. Sanders, Paul Seymour en Robin Thomas, ‘A

new proof of the four-colour theorem’, Electronic Research Announcements of

the American Mathematical Society, Vol. 2, No. 1 (1996)



[Robertson1997] Neil Robertson, Daniel P. Sanders, Paul Seymour en Robin Thomas,

‘The four-colour theorem’, Journal of Combinatorial Theory, Series B, Vol. 70,

No. 1 (1997), pp. 2-44



[Robinson1965] John Alan Robinson, ‘A machine-oriented logic based on the resolution

principle’, Journal of the Association for Computing Machinery, Vol. 12 (1965),

pp. 23-41



[Robinson2001] , Alan Robinson, Andrei Voronkov, Handbook of Automated Reasoning

(2001), Elsevier Science Publishers



[Rota1985] Gian-Carlo Rota en David H. Sharp, ‘Mathematics, Philosophy, and Artificial

Intelligence’, Los Alamos Science, No. 12 (1985), pp. 92-104



[Rota1997] Gian-Carlo Rota, ‘The phenomenology of mathematical beauty’, Synthese,

Vol. 111, No. 2 (1997), pp. 171-182



[Rota1997b] Gian-Carlo Rota, ‘The phenomenology of mathematical proof’, Synthese,

Vol. 111, No. 2 (1997), pp. 183-196, in [Jacquette2001], pp. 218-225



[Ryser1955] Herbert J. Ryser, ‘Geometries and incidence matrices’, The American Mathematical

Monthly, Vol. 62, No. 7 (1955), pp. 25-31



[Saaty1972] Thomas L. Saaty, ‘Thirteen colorful variations on Guthrie's Four-Color Conjecture’,

The American Mathematical Monthly, Vol. 79, No. 1 (1972), pp. 2-43



[Sandborg1998] David Sandborg, ‘Mathematical explanation and the theory of whyquestions’,

The British Journal for the Philosophy of Science, Vol. 49, No. 4

(1998), pp. 603-624



[Shankar1988] Natarajan Shankar, ‘A mechanical proof of the Church-Rosser theorem’,

Journal of the Association for Computing Machinery, Vol. 35, No. 3 (1988), pp.

475-522



[Shankar2002] Natarajan Shankar, ‘Little engines of proof’, Proceedings of FME 2002:

Formal Methods - Getting IT Right (2002), pp. 1-20



[Simpson2004] Carlos Simpson, ‘Computer theorem proving in mathematics’, Letters in

Mathematical Physics, Vol. 69 (2004), pp. 287-315



[Singh1998] Simon Singh (ed.), Het laatste raadsel van Fermat, Het verhaal van een

stelling die de grootste geesten der aarde 358 jaar lang tot wanhoop dreef (1998),

De Arbeiderspers, pp. 367



[Solovay1977] Robert M. Solovay en Volker Strassen, ‘A fast Monte-Carlo test for primality’,

SIAM Journal on Computing, Vol. 6, No. 1 (1977), pp. 84-85



[Spencer1983] Joel Spencer, ‘Long proofs’, The American Mathematical Monthly, Vol.

90, No. 6 (1983), pp. 365-366



[Steel2000] Graham Steel, Simon Colton, Alan Bundy en Toby Walsh, ‘Cross-domain

mathematical concept formation’, Proceedings of the AISB'00 Symposium on Creative

and Cultural Aspects and Applications of AI and Cognitive Science (2000)



[Steiner1978] Mark Steiner, ‘Mathematical explanation’, Philosophical Studies, Vol. 34

(1978), pp. 135-151, in [Jacquette2001], pp. 30-39



[Swart1980] Edward R. Swart, ‘The philosophical implications of the four-color theorem’,

The American Mathematical Monthly, Vol. 87, No. 9 (1980), pp. 697-707



[Szpiro2003] George Szpiro, ‘Does the proof stack up?’, Nature, Vol. 424 (2003), pp.

12-13



[Szpiro2003b] George Szpiro, Kepler's conjecture, How some of the greatest minds in

history helped solve one of the oldest math problems in the world (2003), Wiley,

pp. 272



[Tao2007] Terence Tao, ‘What is good mathematics?’, Bulletin of the American Mathematical

Society, Vol. 44 (2007)



[Teller1980] Paul Teller, ‘Computer proof’, The Journal of Philosophy, Vol. 77, No. 12

(1980), pp. 797-803



[Thiele2002] Ruediger Thiele en Larry Wos, ‘Hilbert's twenty-fourth problem’, Journal

of Automated Reasoning, Vol. 29, No. 1 (2002), pp. 67-89



[Thomas1998] Robin Thomas, ‘An update on the four-color theorem’, Notices of the

American Mathematical Society, Vol. 45, No. 7 (1998), pp. 848-859



[Thurston1994] William P. Thurston, ‘On proof and progress in mathematics’, Bulletin of

the American Mathematical Society, Vol. 30, No. 2 (1994), pp. 161-177, in [Tymoczko1998],

pp. 337-356



[Turing1936] Alan M. Turing, ‘On computable numbers, with an application to the Entscheidungsproblem’,

Proceedings of the London Mathematical Society, series 2,

Vol. 42 (1936), pp. 230-265



[Tymoczko1979] Thomas Tymoczko, ‘The four-color problem and its philosophical significance’,

The Journal of Philosophy, Vol. 76, No. 2 (1979), pp. 57-83, in [Tymoczko1998],

pp. 243-266



[Tymoczko1980] Thomas Tymoczko, ‘Computers, proofs and mathematicians: a philosophical

investigation of the four-color proof’, Mathematics Magazine, Vol. 53,

No. 3 (1980), pp. 131-138



[Tymoczko1981] Thomas Tymoczko, ‘Computer use to computer proof: a rational reconstruction’,

The Two-Year College Mathematics Journal, Vol. 12, No. 2 (1981),

pp. 120-125



[Tymoczko1998] Thomas Tymoczko (ed.), New Directions in the Philosophy of Mathematics

(1998), Princeton University Press, pp. 448



[VanBendegem1988] Jean-Paul Van Bendegem, ‘Non-formal properties of real mathematical

proofs’, Proceedings of the 1988 Biennial Meeting of the Philosophy of

Science Association (1988), pp. 249-254



[VanBendegem2003] Jean-Paul Van Bendegem, ‘Thought experiments in mathematics:

anything but proof’, Philosophica, Vol. 72 (2003), pp. 9-33



[VanDenEssen2006] Arno van den Essen, Magische vierkanten, Van Lo-Shu tot sudoku.

De wonderbaarlijke geschiedenis van wiskundige puzzels (2006), Veen Magazines,

pp. 238



[VanFraassen1980] Bas van Fraassen, The Scientific Image (1980), Clarendon Press, Oxford



[Veroff2000] Robert Veroff, Reasoning at multiple levels of abstraction, Technical Report

TR-CS-2000-50 (2000),

http://www.cs.unm.edu/~treport/tr/00-10/multiplelevels.ps.gz, Department of

Computer Science, University of New Mexico



[Veroff2001] Robert Veroff, ‘Solving open questions and other challenge problems using

proof sketches’, Journal of automated reasoning, Vol. 27, No. 2 (2001), pp.

157-174



[Veroff2002] Robert Veroff, Solution to a Challenge Problem in HBCK, Tech. Report

TR-CS-2002-32, Computer Science Department, University of New Mexico

(2002)



[Walsh1992] Toby Walsh, Alex Nunes en Alan Bundy, ‘The use of proof plans to sum

series’, Proceedings of the 11th International Conference on Automated Deduction

(1992), pp. 325-339



[Wang1960] Hao Wang, ‘Toward mechanical mathematics’, IBM Journal of Research

and Development, Vol. 4, No. 1 (1960), pp. 2-22



[Wang1960b] Hao Wang, ‘Proving theorems by pattern recognition I’, Communications

of the ACM, Vol. 3, No. 4 (1960), pp. 220-234



[Wang1998] Hao Wang, ‘Theory and practice in mathematics’, in [Tymoczko1998], pp.

129-152



[Weber2002] Erik Weber en Liza Verhoeven, ‘Explanatory proofs in mathematics’, Logi-

que & Analyse, Vol. 179-180 (2002), pp. 299-307



[Wiedijk2003] Freek Wiedijk, ‘Formal proof sketches’, Wan Fokkink, Jaco van de Pol,

7th Dutch Proof Tools Day (2003)



[Wiedijk2004] Freek Wiedijk, ‘Formal proof sketches’, Stefano Berardi, Mario Coppo,

Ferruccio Damiani, Lecture Notes in Computer Science, Types for Proofs and

Programs: Third International Workshop, Vol. 3085 (2004), pp. 378-393



[Wiedijk2006] Freek Wiedijk, ‘On the usefulness of formal methods’, Nieuwsbrief van

de NVTI (2006), pp. 14-23



[Womack2003] Catherine Womack en Martin Farach, ‘Randomization, persuasiveness

and rigor in proofs’, Synthese, Vol. 134 (2003), pp. 71-84



[Wos2001] Larry Wos, ‘A milestone reached and a secret revealed’, Journal of Automated

Reasoning, Vol. 27, No. 2 (2001), pp. 89-95



[Wos2002] Larry Wos en Branden Fitelson, ‘The automation of sound reasoning and

successful proof finding’, in Dale Jacquette (ed.), Blackwell Companion to Philosophical

Logic (2002), Blackwell Publishers



[Wos2003] Larry Wos, Dolph Ulrich en Branden Fitelson, ‘XCB, the last of the shortest

single axioms for the classical equivalential calculus’, Bulletin of the Section Logic,

Vol. 32, No. 3 (2003), pp. 129-134



[Zeilberger1993] Doron Zeilberger, ‘Theorems for a prize: Tomorrow's semi-rigorous

mathematical culture’, Notices of the American Mathematical Society, Vol. 40

(1993), pp. 978-981



[Zwick2002] Uri Zwick, ‘Computer assisted proof of optimal approximability results’,

Proceedings of the thirteenth annual ACM-SIAM symposium on Discrete algorithms

(2002), pp. 496-505

Download scriptie (1.37 MB)
Universiteit of Hogeschool
KU Leuven
Thesis jaar
2007