
International Spring School on
FORMALIZATION OF MATHEMATICS
(MAP 2012)
March, 1216, 2012,
Sophia Antipolis,France 



Program
program at a glance,
updated exercises and solutions for later versions of Coq
8:4510:00 
Registration 
10:0010:40 
Lecture:
Introduction to formalizing mathematics (Y. Bertot)
slides, examples 
10:4012:00 
Laboratory session
exercises, solutions 
12:0012:40

Lecture:
Logics and basic tactics (L. Rideau)
slides 
12:4013:30 
Lunch 
13:3015:20 
Laboratory session
exercises, solutions 
15:2016:00 
Lecture:
Programming in Coq (L. ThÃ©ry)
slides 
16:0018:00 
Laboratory session
exercises,
solutions 
9:009:40 
Lecture:
A first tour of the library (L. Rideau)
slides 
9:4011:30 
Laboratory session
exercises,
solutions 
11:3012:10

Lecture:
Big operations (Y. Bertot)
slides, examples 
12:1013:30 
Lunch 
13:3015:20 
Laboratory session
exercises,
solutions 
15:2016:00 
Lecture:
The algebraic library (A. Mahboubi)
slides 
16:0018: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 
Course contents
Using computers to state and prove theorems
 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
Principles and practice of goal directed proofs
 Basic commands for proofs in Coq/Ssreflect
 Advanced techniques for rewriting an proofs by
induction
 Changing points of views: reflection mechanisms
A guided tour of the ssreflect library
 Basic notions: finite sets, numbers, tuples
 Algebraic notions: polynomials, matrices, vector
spaces
 Structuration principles
 Illustration on an advanced example
Lectures on advanced topics
 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 tradeoffs 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 multitool 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 speedup 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
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.

