Proof Theory |

**In General**

* __Methods of proof__: By contradiction,
by construction, by induction, by exhaustion; Disproof by counterexample.

* __Constructive vs contradiction__:
(Jan Brouwer) If numbers and other mathematical objects do not exist in a Platonic
realm–if they are constructed–then the only acceptable existence proofs
must be recipes for constructing them; 1960s (Errett A Bishop), Most of classical
mathematical analysis can be proved constructively–but one has to abandon the
idea of an infinite set.

* __Checking proofs__: Computer-based proofs
are very difficult/tedious to check; Even in traditional proofs, reviewers rarely check
every step, instead focusing mostly on the major points, and relying also on the author's
track record; In the end, they either believe the proof or not (according to mathematics
historian Akihiro Kanamori "It's like osmosis; More and more people say it's a proof
and you believe them"); > s.a. computation.

> __Online resources__:
see Wikipedia page.

**References**
> s.a. conjectures; Theorems.

@ __Intros__: Lakatos 63 [classic on mathematical discovery and methodology,
Worrall & Zahar ed-15];
Solow 82;
Pohlers 89,
08;
Hayes AS(07).

@ __Textbooks, II__:
Penner 99 [and combinatorics];
Beck & Geoghegan 10;
Gerstein 12;
Cunningham 13 [logical introduction];
Oliveira & Stewart 15;
Meier & Smith 17 [and doing mathematics];
Velleman 19.

@ __Other general references__: Takeuti 75;
Schütte 77 [not standard framework];
Simmons 00 [III, and computation];
Toelstra & Schwichtenberg 00 [III];
Hanna et al ed-10;
Stillwell 10.

@ __Related topics__:
Maclane Syn(97) [physicists and mathematics];
Hughes AM(06) [combinatorics as opposed to syntax].

@ __Proof by computer__: Horgan SA(93)oct;
MacKenzie 01;
Simpson LMP(04) [overview];
Witzel et al a2012
[Python-based interactive theorem-proving assistant];
> s.a. computation.

@ __Quantum proofs__: Aaronson & Kuperberg qp/06 [vs classical proofs].

**Physics-Related and Other Topics**
> see philosophy of science [explanations].

@ __References__: Cohen JSP(09) [example of failure of common opinions and intuitive arguments];
Bolotin APR(16)-a1509 [examples of non-constructive proofs in quantum theory].

main page
– abbreviations
– journals – comments
– other sites – acknowledgements

send feedback and suggestions to bombelli at olemiss.edu – modified 9 feb 2021