Mathematical Components Manifesto

 

 

Georges Gonthier

Benjamin Werner

Yves Bertot

 

The research area of Computer Assisted Reasoning comprises the activities related to the development, the study and the use of proof assistants, i.e., computer systems that support the development of mathematical formalisms, models and theories. Despite the mathematical origins, progress in computer assisted reasoning has mostly been driven by applications in computer science, and this is where its most prominent successes lie: in hardware verification, where computer assisted reasoning is widely used, and in protocol security verification, where it is increasingly popular.

 

Paradoxically, computer assisted reasoning has yet to gain widespread acceptance in its original domain of application, mathematics. This state of affairs is commonly attributed to a “lack of libraries”: to do a proof of any significance, most of the basic, common mathematical knowledge has to be developed from scratch. This is a showstopper in the highly scholarly field of mathematics, where many works are built upon the concepts and results of others. This is much less of an issue for computer science applications, which tend to require a large number of proofs in a fixed basic theory; this characteristic makes it easier to leverage the processing power of proof assistants.

 

Obviously, the lack of good mathematical libraries is due to the difficulty of creating and using them. The most commonly cited causes for this difficulty are rather superficial, such as poor input and display notation, poor lookup and retrieval, insufficient automation of deduction. It is our thesis that the “library” concept itself is at fault, more precisely the notion that a mathematical library consists of a set of symbols and a collection of first-order theorems for using these symbols. For to use such a library one must adhere exactly to its conventions and this all but rules out the “abuses of notation that make mathematics tractable” (Bourbaki).

 

The situation has a parallel in software engineering, where development based on procedure libraries hit a complexity barrier that was only overcome by switching to a more flexible linkage model, combining dynamic dispatch and reflection, to produce software components that are much easier to combine. Our own experience with the proof of the Four Colour Theorem suggests that embedding small symbolic programs in the formulation of a theory in higher-order logic can provide similar flexibility in the development of mathematics, and allow the creation of mathematical components.

 

The purpose of our project would be to pursue and validate this thesis. Since nearly all the major proof assistants (in particular, the Coq system which we would be using) provide the necessary higher-order and computational features we will focus on developping usage patterns for these features, a proof description language that supports these patterns, and a set of mathematical components that will both enrich and illustrate the basic proof language.

 

To focus, drive, and validate the development of this proof technology, we plan to undertake two significant mathematical developments, respectively in numerical computation and group theory.

 

The numerical computation development would extend significanly the capabilities of the Coq system for performing and reasoning about numerical computation. The work would involve both extensions to the Coq system core and the creation of an extended set of mathematical components for numerical algorithms – as we explain below, the two are tightly linked. This development would capitalize on the theorem proving platform and current and planned work in projets Marelle and Logical, respectively. It would be immediately useful for several other projects using the Coq system – notably the verification of the proof of the Kepler Conjecture.

 

The group theory development would tackle one of the landmark results of the 20th century in the theory of finite group, and would involve the creation of an extended set of mathematical components for modern algebra. The final target would be the Feit-Thompson (or Odd Order) theorem, which gives the structure of all finite groups with an odd number of elements, and whose textbook proof is over 250 pages, on top of 300 pages of prerequisites. The main purpose of this development is to demonstrate that our theorem-proving platform is suitable for “mainstream” mathematics, as the use of proof assistants have been strongly biased towards logic, combinatorics and theoretical computer science.

 

References

 

1.      H. Barendregt and F. Wiedijk, ‘The Challenge of Computer Mathematics’, Transactions A of the Royal Society, 363 (1835): 2351-2375.

2.      G. Barthe and P. Courtieu, ‘Efficient reasoning about executable specifications in Coq’, Proc. TPHOL'02, Springer-Verlag LNCS 2410 (2002), 31–46.

3.      H. Bender and G. Glauberman, Local Analysis for the Odd Order Theorem, London Math. Soc. LNS 188, Cambridge U. Press, 1994.

4.      Y. Bertot, ‘Vérification formelle d’extraction de racines entières’, INRIA Research Report 5344 (2004).

5.      Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Construction, Texts in Theoretical Computer Science, an EATCS series. Springer Verlag, 2004.

6.      Y. Bertot, N. Magaud, and P. Zimmermann, ‘A proof of GMP square root’, J. Automated Reasoning 29 (2002), 225–252.

7.      S. Boldo, M. Daumas, and L. Théry, ‘Formal proofs and computations in finite precision arithmetic’, Proc. Calculemus 2003.

8.      S. Boutin, ‘Using reflection to build efficient and certified decision procedures’, Proc. TACS’97, Springer-Verlag LNCS 1281, 1997.

9.      M. Daumas, C. Moreau-Finot, and L. Théry, ‘Computer validated proofs of a toolset for adaptable arithmetic’, INRIA Report 4095 (2001).

10.  M. Daumas, L. Rideau, and L. Théry, ‘A generic library of floating-point numbers and its application to exact computing,’ Proc. TPHOL’01, Springer-Verlag LNCS 2152 (2001), 169–184.

11.  W. Feit and J. G. Thompson, ‘Solvability of Groups of Odd Order’, Pacific J. Math. 13 (1963), 775–1029.

12.  H. Geuvers, R. Pollack, F. Wiedijk and J. Zwanenburg, ‘A Constructive Algebraic Hierarchy in Coq’, J. Symbolic Computation 34(4) (2002) 271–86.

13.  G. Gonthier, ‘A computer-checked proof of the Four Colour Theorem’, prepublication.

14.  P. Gorenstein, Finite Groups, Chelsea Publishing, New York, 1980.

15.  F. Kammüller and L. C. Paulson, ‘A formal proof of Sylow's theorem: An experiment in abstract algebra with Isabelle Hol’, J. Autom. Reasoning 23(3-4): 235–264 (1999).

16.  T. Peterfalvi, Character Theory for the Odd Order Theorem, London Math. Soc. LNS 272, Cambridge U. Press, 2000.

17.  N. Robertson, D. Sanders, P. Seymour, and R. Thomas. ‘The Four-Colour Theorem’, J. Combinatorial Theory, Series B 70 (1997), 2–44.

 

Personal tools