International Spring School on
FORMALIZATION OF MATHEMATICS
(MAP 2012)
March, 12-16, 2012, Sophia Antipolis,France
- Why trust a computer to check proofs, and what to trust?
- Typed formulas, quantifications, and logical connectives
- Using theorems as functions
- Modeling the mathematical practice of notation abuse
- Basic commands for proofs in Coq/Ssreflect
- Advanced techniques for rewriting an proofs by induction
- Changing points of views: reflection mechanisms
- Basic notions: finite sets, numbers, tuples
- Algebraic notions: polynomials, matrices, vector spaces
- Structuration principles
- Illustration on an advanced example
- Georges Gonthier Design and
architecture of the background theories for the Odd
Order Theorem
One of the main objectives of the Odd Order formalization project was to understand how to organize a large working mathematical corpus. The project is nearing completion, with almost all the background and about 80% of the actual proof done, so there is now sufficient experience to judge how well the corpus works. In this talk I will explain and assess some of the trade-offs we made between generality, flexibility, robustness and constructivity, in the design of our theory library, and their impact on usability.
- Thomas C. Hales Lessons from the Flyspeck Formalization
Project
The Flyspeck project aims to give a formal proof of the statement that the densest packing of congruent balls in Euclidean space is the familiar cannonball arrangement. This project is approaching completion: the 300 page text part of the proof has fewer than 500 lines of informal text left to formalize. This talk will discuss some of the lessons learned.
- Julio Rubio Formalization of Mathematics: why Algebraic
Topology?
In our days, many parts of mathematics are being studied from the point of view of their formalization by means of mechanized proof assistants. Nevertheless, mathematics is a so wide discipline that most of its areas have not attracted (yet?) the interest of formalization engineers. Why Algebraic Topology, a rather esoteric part of pure mathematics, is being analyzed formally in these last years? We will try to answer this question in the talk, focusing on the computer algebra system called Kenzo, and on our multi-tool approach (using Isabelle/HOL, Coq/SSReflect and ACL2) to formally specify and verify Kenzo.
- Bas Spitters From computational
analysis to thoughts about analysis in HoTT
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide a fast implementation of the exact real numbers in the Coq proof assistant. Our implementation improves on an earlier implementation by O'Connor by using type classes to describe an abstract specification of the underlying dense set from which the real numbers are built. In particular, we used dyadic rationals built from Coq's machine integers to obtain a 100 times speed up of the basic operations already. We extend the algebraic hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. This hierarchy, based on type classes, allows us to share theory on the naturals, integers, rationals, dyadics, and reals in a convenient way. Finally, we obtain another dramatic speed-up by avoiding evaluation of termination proofs at runtime. Starting from these developments, I will outline how we could improve this development by using Voevodsky's univalence axiom and forcing technology.
- Vladimir Voevodsky Designing a universe polymorphic type system
Program
program at a glance, updated exercises and solutions for later versions of Coq
| Monday 12 |
| 8:45-10:00 | Registration |
| 10:00-10:40 | Lecture: Introduction to formalizing mathematics (Y. Bertot) slides, examples |
| 10:40-12:00 | Laboratory session exercises, solutions |
| 12:00-12:40 |
Lecture:
Logics and basic tactics (L. Rideau) slides |
| 12:40-13:30 | Lunch |
| 13:30-15:20 | Laboratory session exercises, solutions |
| 15:20-16:00 | Lecture: Programming in Coq (L. Théry) slides |
| 16:00-18:00 | Laboratory session exercises, solutions |
| Tuesday 13 |
| 9:00-9:40 | Lecture: Changing points of view (P.-Y. Strub) slides, examples |
| 9:40-11:30 | Laboratory session exercises, solutions |
| 11:30-12:10 |
Lecture: More advanced tactics (E. Tassi) slides |
| 12:10-13:30 | Lunch |
| 13:30-15:20 | Laboratory session exercises, solutions |
| 15:20-16:00 | Lecture: Canonical Structures (A. Mahboubi) slides |
| 16:00-18:00 | Laboratory session exercises, solutions |
| Wednesday 14 |
| 9:00-9:40 | Lecture: A first tour of the library (L. Rideau) slides |
| 9:40-11:30 | Laboratory session exercises, solutions |
| 11:30-12:10 |
Lecture: Big operations (Y. Bertot) slides, examples |
| 12:10-13:30 | Lunch |
| 13:30-15:20 | Laboratory session exercises, solutions |
| 15:20-16:00 | Lecture: The algebraic library (A. Mahboubi) slides |
| 16:00-18:00 | Laboratory session exercises, solutions |
| Advanced exercises | On big operations and
binomials: counting subsets of odd and even cardinals in
any finite set (proposed by J.Grimm). On fintypes: Showing that in any group of more than 1 person, there are two persons with the same number of friends (proposed by L. Théry). |
| Gala Dinner Restaurant Bijou Plage |
| Thursday 15 |
| 9:00-9:40 | Lecture: Advanced topic on finite groups (E. Tassi) slides, examples |
| 9:40-11:30 | Laboratory session exercises, solutions |
| 11:30-12:10 |
Lecture: Advanced topic on the Cayley-Hamilton theorem (P.-Y. Strub) slides |
| 12:10-13:30 | Lunch |
| 13:30-15:20 | Laboratory session exercises, solutions |
| 15:20-16:00 | Lecture: Advanced topic on linear algebra (L. Théry) slides |
| 16:00-17:30 | Laboratory session exercises, solutions |
| 17:30-18:30 | Invited lecture: Formalization of Mathematics: why Algebraic Topology? (Julio Rubio) |
| Friday 16 |
| 9:00-10:00 | Invited lecture: Designing a universe polymorphic type system (Vladimir Voevodsky) |
| 10:30-11:30 | Invited lecture: From computational analysis to thoughts about analysis in HoTT (Bas Spitters) |
| 12:00-13:30 | Lunch |
| 13:30-14:30 | Invited lecture: Lessons from the Flyspeck Formalization Project (Thomas Hales) |
| 15:00-16:00 | Invited lecture: Design and architecture of the background theories for the Odd Order Theorem (Georges Gonthier) |
Course contents
Using computers to state and prove theorems
Principles and practice of goal directed proofs
A guided tour of the ssreflect library
Lectures on advanced topics
I will tell about my recent work the goal of which is to design a fully universe polymorphic type system which can be extended with resizing rules.
| webmaster |