# [TYPES/announce] CfPart: School on Formalization of Mathematics (March 12-16, 2012, Sophia Antipolis, France)

Yves Bertot yves.bertot at inria.fr
Mon Nov 28 10:31:32 EST 2011

```International Spring School
on
FORMALIZATION OF MATHEMATICS
Sophia Antipolis, France
March 12-16, 2012

http://www-sop.inria.fr/manifestations/MapSpringSchool/

Overview and topics

A growing population of mathematicians, computer scientists, and
engineers use computers to construct and verify proofs of mathematical
results. Among the various approaches to this activity, a fruitful one
relies on interactive theorem proving. When following this approach,
researchers have to use the formal language of a theorem prover to
encode their mathematical knowledge and the proofs they want to
scrutinize. The mathematical knowledge often contains two parts: a
static part describing structures and a dynamic part describing
algorithms. Then proofs are made in a style that is inspired from
usual mathematical practice but often differs enough that it requires
some training. A key ingredient for the mathematical practitioner is
the amount of mathematical knowledge that is already available in the
system's library.

The Coq system is an interactive theorem prover based on Type
Theory. It was recently used to study the proofs of advanced
mathematical results. In particular, it was used to provide a
mechanically verified proof of the four-color theorem and it is now
being used in a long term effort, called Mathematical Components to
verify results in group theory, with a specific focus on the odd order
theorem, also known as the Feit-Thompson theorem. These two examples
rely on a structured library that covers various aspects of finite set
theory, group theory, arithmetic, and algebra.

The aim of this school is to give mathematicians and mathematically
inclined researchers the keys to the Coq system and the Mathematical
Components library. The topics covered are:

Formal proof techniques
Structuring libraries
Encoding of common mathematical structures
Formal description of algorithms
* The odd order theorem
* Constructive algebraic topology
* Kepler's conjecture,
* Computational analysis,
* Foundational investigations.

The school's contents will be organized as a balanced schedule between
lectures and laboratory sessions where participants will be invited to
work on their own computer and try their hands on a progressive
collection of exercises.

Speakers

The current list of speakers is:

Georges Gonthier (Microsoft Research)
Thomas C. Hales (University of Pittsburgh)
Julio Rubio (Universidad de La Rioja)
Yves Bertot (Inria)
Assia Mahboubi (Inria)
Laurence Rideau (Inria)
Enrico Tassi (MSR-Inria common laboratory)
Laurent Théry (Inria)

Registration

The registration fee is 320 Euros. A registration form is available on the web site

http://www-sop.inria.fr/manifestations/MapSpringSchool/

Location

The school will take place at Inria's Sophia Antipolis research center. This center is
located 20 mn by bus from the city Antibes on the Mediterranean sea, nearby
Nice's international airport, with a variety of hotels at a walking distance. Advice for
accomodation is provided on the web page.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20111128/454d7211/attachment-0001.html>
```