Seminar - Formal Proof in Mathematics and Computer Science

Summer Semester 2017

Overview

TitleSeminar - Formal Proof in Mathematics and Computer Science
SemesterSummer Semester 2017
ModuleMaster-Seminar IN2107, Master-Seminar MAXXXX
PrerequisitesAttendants should have already seen a couple of mathematical proofs and should be curious about the foundations and future of mathematics.
SWS2
ECTSComputer Science: 5, Mathematics: 4
WorkloadExpected coursework:
  • 10-page seminar paper
  • two 1-page reviews of other participants' papers
  • 45-minute presentation
OrganizationTobias 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

Workflow

Each student will be assigned a topic based on their preferences and is expected to finish the following 3 tasks:

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

NameTopicPaperSlides
Martin Bullinger11. Formal Proofs – Maths – 4 Color Theorem[PDF][PDF]
Stefan Dirix13. Formal Proofs – CS – C compiler (CompCert)[PDF][PDF]
Kumar Harsha15. Computational Metaphysics[PDF][PDF]
Kevin Kappelmann1. Foundations of Mathematics and Grundlagenkrise[PDF][PDF]
Stefan Kober12. Formal Proofs – Maths – Kepler Conjecture[PDF][PDF]
Sebastian Neubauer5. Systems – Isabelle/HOL[PDF][PDF]
Karl Rädle6. Systems – Coq[PDF][PDF]
Alexej Rotar9. Machine Learning on Knowledgebases[PDF][PDF]
Élise Tasso2. Systems – Mizar[PDF][PDF]
Felix Wruck8. Automatic Theorem Provers[PDF][PDF]
Lukas Wüsteney14. Formal Proofs – CS – Mikrokernel (seL4)[PDF][PDF]
Yuchang Zhang8. Automatic Theorem Provers[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 12, 13)
Date: 18.07.2017 (topics 14, 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:

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.