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 pageabbreviationsjournalscommentsother sitesacknowledgements
send feedback and suggestions to bombelli at olemiss.edu – modified 9 feb 2021