Seminar - Formal Proof in Mathematics and Computer Science
Summer Semester 2017
Overview
| Title | Seminar - Formal Proof in Mathematics and Computer Science |
| Semester | Summer Semester 2017 |
| Module | Master-Seminar IN2107, Master-Seminar MAXXXX |
| Prerequisites | Attendants should have already seen a couple of mathematical proofs and should be curious about the foundations and future of mathematics. |
| SWS | 2 |
| ECTS | Computer Science: 5, Mathematics: 4 |
| Workload | Expected coursework:
|
| Organization | Tobias Nipkow, Michael Prähofer, Max P. L. Haslbeck, Ondřej Kunčar |
Don't miss the kickoff meeting on January 25th!
Content
Pierre Deligne: “I don't believe in a proof done on a computer. In a way, I
am very egocentric. I believe in a proof if I understand it, if it's clear.
A computer will also make mistakes, but they are much more difficult to
find.”
Paul Erdös: “I’m not an expert on the four color problem, but I assume the
proof is true. However, it’s not beautiful. I’d prefer to see a proof that
gives insight into why four colors are sufficient.”
What is a proof and how can I persuade somebody that I am right? Must a
proof be elegant? Do I have to understand the proof or is it enough to see
that every step is correct? What if only one person in the world understands
the proof. Is it a proof? Has a 5GB proof generated by a computer the same
credibility as a human-written proof?
The notion of proof, as a question what constitutes an argument that
something is true, has been evolving throughout time. In the seminar, we
will first take the historical perspective and cover the main steps in this
evolution: from an appeal to intuition (infinitesimal calculus) throughout
the foundational crisis at the beginning of the 20th century
(Grundlagenkris, Principia Mathematica, Gödel) to a provocative question
whether we have been recently experiencing a new crisis (incomprehensible
proofs).
As any other field of human activity, specialization did not avoid
mathematics either. The proofs are getting more abstract and advanced and
are understandable for a constantly smaller and smaller community of
experts. In addition, more and more proofs are generated by computers
nowadays. In the seminar, we will look at concrete examples of such proofs
and discuss how they pose a challenge to the notion of proof.
Last but not least, we will look at a possible answer to the crisis:
proofs written in a computer and checked by a computer. We will
focus on three main groups of interactive theorems provers (based on set
theory (Mizar), higher-order logic (HOL) and type theory (Coq)). We will
look at both their logical foundations and user perspective.
Overview Material
- Thomas C. Hales, Formal Proof
- Freek Wiedijk, Formal proof – getting started
Workflow
Each student will be assigned a topic based on their preferences and is expected to finish the following 3 tasks:
- Compile a 10-page paper about the topic.
- Prepare and give a 45-minute presentation of the paper's content.
- Review two papers of other participants.
More details about the dates and deadlines can be found in the section 'Dates' below.
Language
This seminar is held in English. The scientific paper, the review as well as the presentation should be held in English.
Hand-in
All the documents due should be sent to Ondřej Kunčar.
Course Registration
The computer science students should use the matching system. Math students please follow these guidelines.
Assignment of Seminar Topics
The assignment of seminar topics will be based on students' preferences. Details will be announced later.
Master Thesis
It is possible to continue with the topic and turn it into a suitable master thesis.
Topic Assignment
| Name | Topic | Paper | Slides |
|---|---|---|---|
| Martin Bullinger | 11. Formal Proofs – Maths – 4 Color Theorem | [PDF] | [PDF] |
| Stefan Dirix | 13. Formal Proofs – CS – C compiler (CompCert) | [PDF] | [PDF] |
| Kumar Harsha | 15. Computational Metaphysics | [PDF] | [PDF] |
| Kevin Kappelmann | 1. Foundations of Mathematics and Grundlagenkrise | [PDF] | [PDF] |
| Stefan Kober | 12. Formal Proofs – Maths – Kepler Conjecture | [PDF] | [PDF] |
| Sebastian Neubauer | 5. Systems – Isabelle/HOL | [PDF] | [PDF] |
| Karl Rädle | 6. Systems – Coq | [PDF] | [PDF] |
| Alexej Rotar | 9. Machine Learning on Knowledgebases | [PDF] | [PDF] |
| Élise Tasso | 2. Systems – Mizar | [PDF] | [PDF] |
| Felix Wruck | 8. Automatic Theorem Provers | [PDF] | [PDF] |
| Lukas Wüsteney | 14. Formal Proofs – CS – Mikrokernel (seL4) | [PDF] | [PDF] |
Dates
The Kickoff Meeting
Date: January 25th, 5pm
Place: Turing, MI 00.09.038
What: We strongly recommend the students that are interetsted
in the seminar to come as well as the students that have still doubts and would like to learn more about the topic or
organization.
Deadlines for The Paper Drafts
Date: 09.05.2017 (topics 1, 2)
Date: 16.05.2017 (topics 5, 6)
Date: 23.05.2017 (topics 8, 9)
Date: 30.05.2017 (topic 11)
Date: 06.06.2017 (topics 12, 13)
Date: 13.06.2017 (topics 14, 15)
Deadlines for The Slide Drafts
Date: 23.05.2017 (topics 1, 2)
Date: 30.05.2017 (topics 5, 6)
Date: 06.06.2017 (topics 8, 9)
Date: 13.06.2017 (topic 11)
Date: 20.06.2017 (topics 12, 13)
Date: 27.06.2017 (topics 14, 15)
Deadlines for The Reviews
Every student will get two papers to review between 09.05. and 13.06. and will be supposed to submit each review in 2 weeks.
Presentations and Deadlines for The Final Versions
Date: 13.06.2017 (topics 1, 2)
Date: 20.06.2017 (topics 5, 6)
Date: 27.06.2017 (topics 8, 9)
Date: 04.07.2017 (topic 11)
Date: 11.07.2017 (topics 13, 14)
Date: 18.07.2017 (topics 12, 15)
Time: 14:00 - 16:00
Place: MI 00.09.038 (Turing)
Topics
Except for four standalone topics (foundations of math, automatic theorems provers, machine learning and computational metaphysics), the topics fall into two main categories:
- Proof assistants (Mizar, Isabelle and Coq). Each system is covered by possibly two seperate presentations: logical foundations and a practical demonstration of how to use the system.
- Example of formal proofs that were formalized in a proof assistant and/or pose a challenge to the notion of proof.
1. Foundations of Mathematics and Grundlagenkrise
Description: At the beginning of the 20th century it became clear that mathematics needed formal foundations, which was partly caused by discovering various paradoxes. A couple of solutions were proposed including Hilbert's program of formalism. The crisis was partially solved by adopting the new foundations of set theory although Hilbert's ambitions were not completely fulfilled due to Gödel. The student should cover main events and players from this story and accompany the presentation by the most
important technical details.
References:
[1] T. Gowers et al. The Princeton Companion to Mathematics, Princeton Univ. Press, 2008
[2] A.A. Fraenkel, Y. Bar-Hillel, A. Levy. Foundations of Set Theory, North-Holland, 1973
[3] P. J. Davis, R. Hersh. The Mathematical Experience, Birkhäuser, 2012
[4] B. Robič. The Foundations of Computability Theory, Springer, 2015
Advisor: Ondřej Kunčar
2. Systems – Mizar Foundations
Description: Mizar is a real pioneer among interactive provers. It dates its history back into the 70’s. The system is unique because of its foundation (first-order set theory with an involved soft-typing type system), which is close to the standard mathematical language and which differs from foundations of other mainstream provers. The student should introduce the logical foundations of Mizar including the type system.
References:
[1] J. Harrison, J. Urban and F. Wiedijk. History of Interactive Proving
[2] A. Grabowski, A. Korniłowicz, A. Naumowicz. Mizar in a Nutshell
[3] F. Wiedijk. Mizar's Soft Type System
Advisor: Ondřej Kunčar
3. Systems – Mizar Demo
Description: Mizar is a real pioneer among interactive provers. It dates its history back into the 70’s. The system is unique because of its foundation (first-order set theory with an involved soft-typing type system), which is close to the standard mathematical language and which differs from foundations of other mainstream provers. The student should practically demonstrate how to write proofs in Mizar and the typical workflow.
References:
[1] F. Wiedijk. http://www.cs.ru.nl/~freek/courses/pa-2012
[2] F. Wiedijk. Writing a Mizar article in nine easy steps
[3] J. Urban. Mizar-hammer
Advisor: Ondřej Kunčar
4. Systems – HOL Foundations
Description: HOL is a family of proof assistants that use a similar variant of a higher-order logic (a form of classic set theory typed using simple types with rank-1 polymorphism) and are implemented by using a small inference kernel (the LCF approach). The design goal was to use a logic that is simple but provides enough expressiveness. The student should introduce HOL's logic and compare it with first-order set theory.
References:
[1] J. Harrison, J. Urban and F. Wiedijk. History of Interactive Proving
[2] M.J.C. Gordon, T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press (1993)
[3] O. Kunčar, A. Popescu. A Consistent Foundation for Isabelle/HOL
Advisor: Simon Wimmer
5. Systems – Isabelle/HOL Demo
Description: Isabelle/HOL is one of the most successful proof assistants from the HOL family. The assistant benefits from a powerful automation and uses a proof language, which was inspired by Mizar and which was designed to be close to the declarative mathematical language. The student should practically demonstrate how to write proofs in Isabelle and provide an overview of its many features.
References:
[1] T. Nipkow. Programming and proving in Isabelle/HOL
[2] Isabelle's Documentation
Advisor: Simon Wimmer
6. Systems – Coq Foundations
Description: Coq uses an expressive type theory as a foundation (calculus of inductive constructions) and implements a higher-order logic with dependent types. The student should introduce foundations of Coq and compare it with set theory and HOL.
References:
[1] J. Harrison, J. Urban and F. Wiedijk. History of Interactive Proving
[2] Y. Bertot. Lambda-calculus and types
[3] R. Nederpelt, H. Geuvers. Type Theory and Formal Proofs, Cambridge University Press, 2014
[4] T. Coquand, G. Huet. The Calculus of Constructions, Information and Computation, 76, pp. 95–120, 1988
[5] Ch. Paulin. Inductive Definitions in the system Coq - Rules and Properties. TLCA 1993. pp. 328-345
Advisor: Lars Hupel
7. Systems – Coq Demo
Description: Coq uses an expressive type theory as a foundation (calculus of inductive constructions) and implements a higher-order logic with dependent types. The user should demonstrate how to write proofs in Coq and provide an overview of Coq's heterogeneous environment.
References:
[1] Y. Bertot. Coq in a Hurry
[2] B. C. Pierce et al. Software Foundations
[3] Various other tutorials at the Coq webpage
Advisor: Lars Hupel
8. Automatic Theorem Provers
Description: Automatic theorem provers are tools that can automatically find proofs for mathematical statements. They could already solve a couple of open problems in mathematics, especially
in algebra. Over the last few years, they played a major role in bringing more automation into interactive proof assistants. The student should present
a historical overview of the field, major achievements and sketch how the resolution provers work.
References:
[1] D. A. Plaisted. A Sketch of the History and State of Automated Deduction
[2] D. A. Plaisted. Automated theorem proving, WIREs Cogn Sci 2014, 5:115–128
[3] L. Bachmair and H. Ganzinger. Rewrite-Based Equational Theorem Proving With Selection and Simplification
[4] Stephan Schulz. System Description: E 1.8
Advisor: Ondřej Kunčar
9. Machine Learning on Knowledgebases
Description: With the ever growing libraries of the distinct proof assistents (e.g. MML for Mizar [1]), automated theorem provers on the one hand are able to reuse lemmas of a large corpus of knowledge, but on the other hand have to efficiently filter relevant information from it. Machine learning techniques have been successfully applied here [2,3]. The student presenting this topic should pick a selection of challenges that arise in this context, define the problem and state which solutions were found in literature.
References:
[1] Mizar Mathematical Library
[2] Alama et al., Premise Selection for Mathematics by Corpus Analysis and Kernel Methods
[3] Blanchette et al., A Learning-Based Fact Selector for Isabelle/HOL
Advisor: Maximilian Haslbeck
10. Formal Proofs – Maths – Robin's Conjecture or proofs found by computers
Description: The Robin's conjecture [1] and the boolean Pythagorean Triples problem [2,3] are two classical respective recent examples of theorems solved by means of automatic proof search. Such proofs may be difficult for humans to read, which raises the question whether they should be considered a proper proof. The student should pick a selection of such proofs, review their historical development, the tools used and their impact and reception.
References:
[1] https://www.cs.unm.edu/~mccune/papers/robbins/
[2] http://www.nature.com/news/two-hundred-terabyte-maths-proof-is-largest-ever-1.19990
[3] Heule et al., Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
Advisor: Julian Brunner
11. Formal Proofs – Maths – 4 Color Theorem
Description: The 4 Color Theorem [1] is a long standing theorem in graph theory, stating that for any planar map no more than 4 colors are required to color the regions of the map such that no two adjacent regions possess the same color. Its proof by Appel et al. in 1976 relies on the exhaustive search for counterexamples by a computer program. It was controversially discussed and not accepted as a proof by all mathematicians. In 2005 Georges Gonthier et al. provided a proof [2] with similar ideas but formally verifying the computer program they rely on.
References:
[1] http://mathworld.wolfram.com/Four-ColorTheorem.html
[2] Georges Gonthier, A computer-checked proof of the Four Colour Theorem
Advisor: Ondřej Kunčar
12. Formal Proofs – Maths – Kepler Conjecture
Description: The Kepler Conjecture tries to settle the question how to pack spheres in the densest possible way. The theorem, which was conjectured by Kepler in 1611, was proven by Hales in 2002 relying also on computer calculations. A team of referees accepted the proof being "99% certain". Hales theirafter set out the "Flyspeck Project" [2] to formally verify the proof, which was completed in 2014.
References:
[1] http://mathworld.wolfram.com/KeplerConjecture.html
[2] https://code.google.com/archive/p/flyspeck/
[3] T. C. Hales, Sphere Packings, I
Advisor: Manuel Eberl
13. Formal Proofs – CS – C compiler (CompCert)
Description: The CompCert project's [1] main result is a formally verified C compiler [2] in Coq. The student should present both the architecture of the software project and its verification.
References:
[1] CompCert project
[2] Leroy, Formal verification of a realistic compiler
Advisor: Maximilian Haslbeck
14. Formal Proofs – CS – Mikrokernel (seL4)
Description: Another highlight in formal verification of software system is the seL4 microkernel [1,2] in Isabelle. The formal proof of its correctness was published in 2009 by Klein et al. [3].
References:
[1] seL4
[2] https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4
[3] Klein et al., seL4: Formal verification of an OS kernel
Advisor: Maximilian Haslbeck
15. Computational Metaphysics
Description: Formal proof can not only be applied to mathematics and computer science. Also in philosophy, especially metaphysics, proof assistents have been applied successfully [1,2] and gives rise to computational metaphysics [3,4].
References:
[1] Benzmüller, Paleo, The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics
[2] Benzmüller, Paleo, Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers
[3] https://mally.stanford.edu/cm/
[4] DFG research project "Computational Metaphysics"
Advisor: Maximilian Haslbeck
Course Work
Assignment of topics to review
Independent of the assignment of topics, each participant will be assigned two other topics to review. The author of an paper will not know who is reviewing his paper, which enables the reviewer to stay anonymous and unbiased.
Draft
Each participant hands in a draft of the scientific paper due five weeks prior to the presentation. A draft is a fully written and complete version of the scientific paper. On its basis another (anonymous) student generates the review.
Review
The reviewer receives the drafts, as soon as the authors handed them in, and has 2 weeks for compiling the review. A review should consist of roughly one page, which then will be made accessible to the original authors of the paper. Within two more weeks the original authors have the opportunity to edit their paper and use the critics. Ultimately the final version of the paper has to be submitted before giving the presentation at the seminar.
The reviews should mainly focus on the content of the paper. It is not necessary - for the reviewer - to further investigate into the topic via the attached bibliography. More important is to comment on the structure of the text, the logic of argumentation and whether the topic is displayed in a way, that a reader can clearly follow without having read the bibliography. Typos and grammar are of minor importance, whereas such improvements are nevertheless helpful for the original author. The form of the review is left to the reviewer: both a list of bullet points and running text is feasible.
Preliminary Slides
Three weeks before the presentation a preliminary version of the slides has to be handed in.
Presentation
The presentation should take no more than 45 minutes. We will have 2-3 presentations per meeting.
Paper
The final version of the paper is due at the day of presentation. Length of the text should be around 10 pages. The form of the paper is left to the author, but should be similar to a scientific paper.
Final Version of Slides
The final version of the slides are handed in as a pdf on the day of presentation.
Grading
The grade is compiled in the following way: 20% Reviews + 40% Presentation + 40% Scientific Paper
Hints
For researching sources, services like Google Scholar can ease searching for scientific papers. With the help of eAccess a lot of such papers can be accessed freely, instead of paying for their download.