Section: Overall Objectives

Scientific challenges, expected impact

Computer-algebra systems have been advertised for decades as software for “doing mathematics by computer” [66] . For instance, computer-algebra libraries can uniformly generate a corpus of mathematical properties about special functions so as to display them on an interactive website. This was recently shown by the computer-algebra component of the team  [22] . Such an automated generation significantly increases the reliability of the mathematical corpus, in comparison to the content of existing static authoritative handbooks. The importance of the validity of these contents can be measured by the very wide audience that such handbooks have had, to the point that a book like  [17] remains one of the most cited mathematical publications ever and has motivated the 10-year-long project of writing its successor  [19] . However, can the mathematics produced “by computer” be considered as true mathematics? More specifically, whereas it is nowadays well established that the computer helps in discovering and observing new mathematical phenomenons, can the mathematical statements produced with the aid of the computer and the mathematical results computed by it be accepted as valid mathematics, that is, as having the status of mathematical proofs? Beyond the reported weaknesses or controversial design choices of mainstream computer-algebra systems, the issue is more of an epistemological nature. It will not find its solution even in the advent of the ultimate computer-algebra system: the social process of peer-reviewing just falls short of evaluating the results produced by computers, as reported by Th. Hales  [45] after the publication of his proof of the Kepler Conjecture about sphere packing.

A natural answer to this deadlock is to move to an alternative kind of mathematical software and to use a proof assistant to check the correctness of the desired properties or formulas. The recent success of large-scale formalization projects, like the Four-Color Theorem of graph theory  [40] , the above-mentioned Kepler Conjecture  [45] , and, very recently, the Odd Order Theorem of group theory(http://www.msr-inria.inria.fr/news/the-formalization-of-the-odd-order-theorem-has-been-completed-the-20-septembre-2012/ ), have increased the understanding of the appropriate software-engineering methods for this peculiar kind of programming. For computer algebra, this legitimates a move to proof assistants now.

The Dynamic Dictionary of Mathematical Functions(http://ddmf.msr-inria.inria.fr/ ) (DDMF)  [22] is an online computer-generated handbook of mathematical functions that ambitions to serve as a reference for a broad range of applications. This software was developed by the computer-algebra component of the team as a project(http://www.msr-inria.inria.fr/projects/dynamic-dictionary-of-mathematical-functions/ ) of the MSR–Inria Joint Centre. It bases on a library for the computer-algebra system Maple, Algolib(http://algo.inria.fr/libraries/ ), whose development started 20 years ago in ÉPI Algorithms(http://algo.inria.fr/ ). As suggested by the constant questioning of certainty by new potential users, DDMF deserves a formal guarantee of correctness of its content, on a level that proof assistants can provide. Fortunately, the maturity of special-functions algorithms in Algolib makes DDMF a stepping stone for such a formalization: it provides a well-understood and unified algorithmic treatment, without which a formal certification would simply be unreachable.

The formal-proofs component of the team emanates from another project of the MSR–Inria Joint Centre, namely the Mathematical Components project (MathComp)(http://www.msr-inria.fr/projects/mathematical-components/ ). Over the last six years, the MathComp group endeavoured to develop computer-checked libraries of formalized mathematics, using the Coq proof assistant  [62] . The methodological aim of the project was to understand the design methods leading to successful large-scale formalizations. The work culminated with the recent completion of a formal proof of the Odd Order Theorem, resulting in the largest corpus of algebraic theories ever machine-checked with a proof assistant and a whole methodology to effectively combine these components in order to tackle complex formalizations. In particular, these libraries provide a good number of the many algebraic objects needed to reason about special functions and their properties, like rational numbers, iterated sums, polynomials, and a rich hierarchy of algebraic structures.

The present team takes benefit from these recent advances to explore the formal certification of the results collected in DDMF. The aim of this project is to concentrate the formalization effort on this delimited area, building on DDMF and the Algolib library, as well as on the Coq system  [62] and on the libraries developed by MathComp.

Use Computer Algebra but Convince Users beyond Reasonable Doubt

The following few opinions on computer algebra are, we believe, typical of computer-algebra users' doubts and difficulties when using computer-algebra systems:

• Fredrik Johansson, expert in the multi-precision numerical evaluation of special functions and in fast computer-algebra algorithms, writes on his blog  [51] : “Mathematica is great for cross-checking numerical values, but it's not unusual to run into bugs, so triple checking is a good habit.” One answer in the discussion is: “We can claim that Mathematica has [...] an impossible to understand semantics: If Mathematica's output is wrong then change the input. If you don't like the answer, change the question. That seems to be the philosophy behind.”

• A professor's advice to students  [58] on using Maple: “You may wish to use Maple to check your homework answers. If you do then keep in mind that Maple sometimes gives the wrong answer, usually because you asked incorrectly, or because of niceties of analytic continuation. You may even be bitten by an occasional Maple bug, though that has become fairly unlikely. Even with as powerful a tool as Maple you will still have to devise your own checks and you will still have to think.”

• Jacques Carette, former head of the maths group at Maplesoft, about a bug  [18] when asking Maple to take the limit limit(f(n) * exp(-n), n = infinity) for an undetermined function f : “The problem is that there is an implicit assumption in the implementation that unknown functions do not `grow too fast'.”

As explained by the expert views above, complaints by computer-algebra users are often due to their misunderstanding of what a computer-algebra systems is, namely a purely syntactic tool for calculations, that the user must complement with a semantics. Still, robustness and consistency of computer-algebra systems are not ensured as of today, and, whatever Zeilberger may provocatively say in his opinion 94  [67] , a firmer logical foundation is necessary. Indeed, the fact is that many “bugs” in a computer-algebra system cannot be fixed by just the usual debugging method of tracking down the faulty lines in the code. It is sort of “by design”: assumptions that too often remain implicit are really needed by the design of symbolic algorithms and cannot easily be expressed in the programming languages used in computer algebra A similar certification initiative has already been undertaken in the domain of numerical computing, in a successful manner  [49] , [25] . It is natural to undertake a similar approach for computer algebra.

Make Computer Algebra and Formal Proofs Help One Another

Some of the mathematical objects that interest us are still totally untouched by formalization. When implementing them and their theory inside a proof assistant, we have to deal with the pervasive discrepancy between the published literature and the actual implementation of computer-algebra algorithms. Interestingly, this forces us to clarify our computer-algebraic view on them, and possibly make us discover holes lurking in published (human) proofs. We are therefore convinced that the close interaction of researchers from both fields, which is what we do in this team, is a strong asset.

For a concrete example, the core of Zeilberger's creative telescoping manipulates rational functions up to simplifications. In summation applications, checking that these simplifications do not hide problematic divisions by 0 is most often left to the reader. In the same vein, in the case of integrals, the published algorithms do not check the convergence of all integrals, especially in intermediate calculations. Such checks are again left to the readers. In general, we expect to revisit the existing algorithms to ensure that they are meaningful for genuine mathematical sequences or functions, and not only for algebraic idealizations.

Another big challenge in this project originates in the scientific difference between computer algebra and formal proofs. Computer algebra seeks speed of calculation on concrete instances of algebraic data structures (polynomials, matrices, etc). For their part, formal proofs manipulate symbolic expressions in terms of abstract variables understood to represent generic elements of algebraic data structures. In view of this, a continuous challenge is to develop the right, hybrid thinking attitude that is able to effectively manage concrete and abstract values simultaneously, alternatively computing and proving with them.

Experimental Mathematics with Special functions

Applications in combinatorics and mathematical physics frequently involve equations of so high orders and so large sizes, that computing or even storing all their coefficients is impossible on existing computers. Making this tractable is an extraordinary challenge. The approach we believe in is to design algorithms of good, ideally quasi-optimal, complexity in order to extract precisely the required data from the equations, while avoiding the computationally intractable task of completely expanding them into an explicit representation.

Typical applications with expected high impact are the automatic discovery and proof of results in combinatorics and mathematical physics for which human proofs are currently unattainable.