Computerbewijzen in de wiskundige praktijk

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