2.1 Scientific challenges, expected impact

The general orientation of our team is described by the short name given to it: Special Functions, that is, particular mathematical functions that have established names due to their importance in mathematical analysis, physics, and other application domains. Indeed, we ambition to study special functions with the computer, by combined means of computer algebra and formal methods.

Computer-algebra systems have been advertised for decades as software for “doing mathematics by computer” 88. 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 possibility was recently shown by the computer-algebra component of the team 41. 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 38 remains one of the most cited mathematical publications ever and has motivated the 10-year-long project of writing its successor 78. 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 66 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 success of large-scale formalization projects, like the Four-Color Theorem of graph theory 61, the above-mentioned Kepler Conjecture 66, and the Odd Order Theorem of group theory, 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 (DDMF) 41 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 of the MSR–Inria Joint Centre. It bases on a library for the computer-algebra system Maple, Algolib, whose development started 20 years ago in project-team Algorithms. 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). Since 2006, the MathComp group has endeavoured to develop computer-checked libraries of formalized mathematics, using the Coq proof assistant 85. The methodological aim of the project was to understand the design methods leading to successful large-scale formalizations. The work culminated in 2012 with the 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 85 and on the libraries developed by the MathComp project.

2.2 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 72: “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 80 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 54 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 91, 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 68, 44. It is natural to undertake a similar approach for computer algebra.

2.3 Make computer algebra and formal proofs help one another

Some of the mathematical objects that interest our team 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 strive to maintain 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.

2.4 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 algorithmic proof of results in combinatorics and mathematical physics for which human proofs are currently unattainable.

2.5 Research axes

The implementation of certified symbolic computations on special functions in the Coq proof assistant requires both investigating new formalization techniques and renewing the traditional computer-algebra viewpoint on these standard objects. Large mathematical objects typical of computer algebra occur during formalization, which also requires us to improve the efficiency and ergonomics of Coq. In order to feed this interdisciplinary activity with new motivating problems, we additionally pursue a research activity oriented towards experimental mathematics in application domains that involve special functions. We expect these applications to pose new algorithmic challenges to computer algebra, which in turn will deserve a formal-certification effort. Finally, DDMF is the motivation and the showcase of our progress on the certification of these computations. While striving to provide a formal guarantee of the correctness of the information it displays, we remain keen on enriching its mathematical content by developing new computer-algebra algorithms.

2.6 Computer algebra certified by the Coq system

Our formalization effort consists in organizing a cooperation between a computer-algebra system and a proof assistant. The computer-algebra system is used to produce efficiently algebraic data, which are later processed by the proof assistant. The success of this cooperation relies on the design of appropriate libraries of formalized mathematics, including certified implementations of certain computer-algebra algorithms. On the other side, we expect that scrutinizing the implementation and the output of computer-algebra algorithms will shed a new light on their semantics and on their correctness proofs, and help clarifying their documentation.

2.7 Better symbolic computations with special functions

Generally speaking, we design algorithms for manipulating special functions symbolically, whether univariate or with parameters, and for extracting algorithmically any kind of algebraic and analytic information from them, notably asymptotic properties. Beyond this, the heart of our research is concerned with parametrised definite summations and integrations. These very expressive operations have far-ranging applications, for instance, to the computation of integral transforms (Laplace, Fourier) or to the solution of combinatorial problems expressed via integrals (coefficient extractions, diagonals). The algorithms that we design for them need to really operate on the level of linear functional systems, differential and of recurrence. In all cases, we strive to design our algorithms with the constant goal of good theoretical complexity, and we observe that our algorithms are also fast in practice.

2.8 Interactive and certified mathematical web sites

In continuation of our past project of an encyclopedia, we ambition to both enrich and certify the formulas about the special functions that we provide online. For each function, our website shows its essential properties and the mathematical objects attached to it, which are often infinite in nature (numerical evaluations, asymptotic expansions). An interactive presentation has the advantage of allowing for adaption to the user's needs. More advanced content will broaden the encyclopedia:

• the algorithmic discussion of equations with parameters, leading to certified automatic case analysis based on arithmetic properties of the parameters;
• lists of summation and integral formulas involving special functions, including validity conditions on the parameters;
• guaranteed large-precision numerical evaluations.

3.1 Studying special functions by computer algebra

Computer algebra manipulates symbolic representations of exact mathematical objects in a computer, in order to perform computations and operations like simplifying expressions and solving equations for “closed-form expressions”. The manipulations are often fundamentally of algebraic nature, even when the ultimate goal is analytic. The issue of efficiency is a particular one in computer algebra, owing to the extreme swell of the intermediate values during calculations.

Our view on the domain is that research on the algorithmic manipulation of special functions is anchored between two paradigms:

• adopting linear differential equations as the right data structure for special functions,
• designing efficient algorithms in a complexity-driven way.

It aims at four kinds of algorithmic goals:

• algorithms combining functions,
• functional equations solving,
• multi-precision numerical evaluations,
• guessing heuristics.

This interacts with three domains of research:

• computer algebra, meant as the search for quasi-optimal algorithms for exact algebraic objects,
• symbolic analysis/algebraic analysis;
• experimental mathematics (combinatorics, mathematical physics, ...).

This view is made explicit in the present section.

3.2 Equations as a data structure

Numerous special functions satisfy linear differential and/or recurrence equations. Under a mild technical condition, the existence of such equations induces a finiteness property that makes the main properties of the functions decidable. We thus speak of D-finite functions. For example, 60 % of the chapters in the handbook 38 describe D-finite functions. In addition, the class is closed under a rich set of algebraic operations. This makes linear functional equations just the right data structure to encode and manipulate special functions. The power of this representation was observed in the early 1990s 90, leading to the design of many algorithms in computer algebra. Both on the theoretical and algorithmic sides, the study of D-finite functions shares much with neighbouring mathematical domains: differential algebra, D-module theory, differential Galois theory, as well as their counterparts for recurrence equations.

3.3 Algorithms combining functions

Differential/recurrence equations that define special functions can be recombined 90 to define: additions and products of special functions; compositions of special functions; integrals and sums involving special functions. Zeilberger's fast algorithm for obtaining recurrences satisfied by parametrised binomial sums was developed in the early 1990s already 92. It is the basis of all modern definite summation and integration algorithms. The theory was made fully rigorous and algorithmic in later works, mostly by a group in Risc (Linz, Austria) and by members of the team 79, 87, 53, 51, 52, 73. The past ÉPI Algorithms contributed several implementations (gfun82, Mgfun53).

3.4 Solving functional equations

Encoding special functions as defining linear functional equations postpones some of the difficulty of the problems to a delayed solving of equations. But at the same time, solving (for special classes of functions) is a sub-task of many algorithms on special functions, especially so when solving in terms of polynomial or rational functions. A lot of work has been done in this direction in the 1990s; more intensively since the 2000s, solving differential and recurrence equations in terms of special functions has also been investigated.

3.5 Multi-precision numerical evaluation

A major conceptual and algorithmic difference exists for numerical calculations between data structures that fit on a machine word and data structures of arbitrary length, that is, multi-precision arithmetic. When multi-precision floating-point numbers became available, early works on the evaluation of special functions were just promising that “most” digits in the output were correct, and performed by heuristically increasing precision during intermediate calculations, without intended rigour. The original theory has evolved in a twofold way since the 1990s: by making computable all constants hidden in asymptotic approximations, it became possible to guarantee a prescribed absolute precision; by employing state-of-the-art algorithms on polynomials, matrices, etc, it became possible to have evaluation algorithms in a time complexity that is linear in the output size, with a constant that is not more than a few units. On the implementation side, several original works exist, one of which (NumGfun77) is used in our DDMF.

3.6 Guessing heuristics

“Differential approximation”, or “Guessing”, is an operation to get an ODE likely to be satisfied by a given approximate series expansion of an unknown function. This has been used at least since the 1970s and is a key stone in spectacular applications in experimental mathematics 50. All this is based on subtle algorithms for Hermite–Padé approximants 40. Moreover, guessing can at times be complemented by proven quantitative results that turn the heuristics into an algorithm 49. This is a promising algorithmic approach that deserves more attention than it has received so far.

3.7 Complexity-driven design of algorithms

The main concern of computer algebra has long been to prove the feasibility of a given problem, that is, to show the existence of an algorithmic solution for it. However, with the advent of faster and faster computers, complexity results have ceased to be of theoretical interest only. Nowadays, a large track of works in computer algebra is interested in developing fast algorithms, with time complexity as close as possible to linear in their output size. After most of the more pervasive objects like integers, polynomials, and matrices have been endowed with fast algorithms for the main operations on them 60, the community, including ourselves, started to turn its attention to differential and recurrence objects in the 2000s. The subject is still not as developed as in the commutative case, and a major challenge remains to understand the combinatorics behind summation and integration. On the methodological side, several paradigms occur repeatedly in fast algorithms: “divide and conquer” to balance calculations, “evaluation and interpolation” to avoid intermediate swell of data, etc. 45.

3.8 Encyclopedias

Handbooks collecting mathematical properties aim at serving as reference, therefore trusted, documents. The decision of several authors or maintainers of such knowledge bases to move from paper books 38, 78, 83 to websites and wikis, for instance for special functions or for integer sequences, allows for a more collaborative effort in proof reading. Another step toward further confidence is to manage to generate the content of an encyclopedia by computer-algebra programs, as is the case with the Wolfram Functions Site or DDMF . Yet, due to the lingering doubts about computer-algebra systems, some encyclopedias propose both cross-checking by different systems and handwritten companion paper proofs of their content. As of today, there is no encyclopedia certified with formal proofs.

3.9 Computer algebra and symbolic logic

Several attempts have been made in order to extend existing computer-algebra systems with symbolic manipulations of logical formulas. Yet, these works are more about extending the expressivity of computer-algebra systems than about improving the standards of correctness and semantics of the systems. Conversely, several projects have addressed the communication of a proof system with a computer-algebra system, resulting in an increased automation available in the proof system, to the price of the uncertainty of the computations performed by this oracle.

3.10 Certifying systems for computer algebra

More ambitious projects have tried to design a new computer-algebra system providing an environment where the user could both program efficiently and elaborate formal and machine-checked proofs of correctness, by calling a general-purpose proof assistant like the Coq system. This approach requires a huge manpower and a daunting effort in order to re-implement a complete computer-algebra system, as well as the libraries of formal mathematics required by such formal proofs.

3.11 Semantics for computer algebra

The move to machine-checked proofs of the mathematical correctness of the output of computer-algebra implementations demands a prior clarification about the often implicit assumptions on which the presumably correctly implemented algorithms rely. Interestingly, this preliminary work, which could be considered as independent from a formal certification project, is seldom precise or even available in the literature.

3.12 Formal proofs for symbolic components of computer-algebra systems

A number of authors have investigated ways to organize the communication of a chosen computer-algebra system with a chosen proof assistant in order to certify specific components of the computer-algebra systems, experimenting various combinations of systems and various formats for mathematical exchanges. Another line of research consists in the implementation and certification of computer-algebra algorithms inside the logic 86, 65, 74 or as a proof-automation strategy. Normalization algorithms are of special interest when they allow to check results possibly obtained by an external computer-algebra oracle 57. A discussion about the systematic separation of the search for a solution and the checking of the solution is already clearly outlined in 71.

3.13 Formal proofs for numerical components of computer-algebra systems

Significant progress has been made in the certification of numerical applications by formal proofs. Libraries formalizing and implementing floating-point arithmetic as well as large numbers and arbitrary-precision arithmetic are available. These libraries are used to certify floating-point programs, implementations of mathematical functions and for applications like hybrid systems.

3.14 Machine-checked proofs of formalized mathematics

To be checked by a machine, a proof needs to be expressed in a constrained, relatively simple formal language. Proof assistants provide facilities to write proofs in such languages. But, as merely writing, even in a formal language, does not constitute a formal proof just per se, proof assistants also provide a proof checker: a small and well-understood piece of software in charge of verifying the correctness of arbitrarily large proofs. The gap between the low-level formal language a machine can check and the sophistication of an average page of mathematics is conspicuous and unavoidable. Proof assistants try to bridge this gap by offering facilities, like notations or automation, to support convenient formalization methodologies. Indeed, many aspects, from the logical foundation to the user interface, play an important role in the feasibility of formalized mathematics inside a proof assistant.

3.15 Logical foundations and proof assistants

While many logical foundations for mathematics have been proposed, studied, and implemented, type theory is the one that has been more successfully employed to formalize mathematics, to the notable exception of the Mizar system 75, which is based on set theory. In particular, the calculus of construction (CoC) 55 and its extension with inductive types (CIC) 56, have been studied for more than 20 years and been implemented by several independent tools (like Lego, Matita, and Agda). Its reference implementation, Coq 85, has been used for several large-scale formalizations projects (formal certification of a compiler back-end; four-color theorem). Improving the type theory underlying the Coq system remains an active area of research. Other systems based on different type theories do exist and, whilst being more oriented toward software verification, have been also used to verify results of mainstream mathematics (prime-number theorem; Kepler conjecture).

3.16 Computations in formal proofs

The most distinguishing feature of CoC is that computation is promoted to the status of rigorous logical argument. Moreover, in its extension CIC, we can recognize the key ingredients of a functional programming language like inductive types, pattern matching, and recursive functions. Indeed, one can program effectively inside tools based on CIC like Coq. This possibility has paved the way to many effective formalization techniques that were essential to the most impressive formalizations made in CIC.

Another milestone in the promotion of the computations-as-proofs feature of Coq has been the integration of compilation techniques in the system to speed up evaluation. Coq can now run realistic programs in the logic, and hence easily incorporates calculations into proofs that demand heavy computational steps.

Because of their different choice for the underlying logic, other proof assistants have to simulate computations outside the formal system, and indeed fewer attempts to formalize mathematical proofs involving heavy calculations have been made in these tools. The only notable exception, which was finished in 2014, the Kepler conjecture, required a significant work to optimize the rewriting engine that simulates evaluation in Isabelle/HOL.

3.17 Large-scale computations for proofs inside the Coq system

Programs run and proved correct inside the logic are especially useful for the conception of automated decision procedures. To this end, inductive types are used as an internal language for the description of mathematical objects by their syntax, thus enabling programs to reason and compute by case analysis and recursion on symbolic expressions.

The output of complex and optimized programs external to the proof assistant can also be stamped with a formal proof of correctness when their result is easier to check than to find. In that case one can benefit from their efficiency without compromising the level of confidence on their output at the price of writing and certify a checker inside the logic. This approach, which has been successfully used in various contexts, is very relevant to the present research project.

3.18 Relevant contributions from the Mathematical Component libraries

Representing abstract algebra in a proof assistant has been studied for long. The libraries developed by the MathComp project for the proof of the Odd Order Theorem provide a rather comprehensive hierarchy of structures; however, they originally feature a large number of instances of structures that they need to organize. On the methodological side, this hierarchy is an incarnation of an original work 59 based on various mechanisms, primarily type inference, typically employed in the area of programming languages. A large amount of information that is implicit in handwritten proofs, and that must become explicit at formalization time, can be systematically recovered following this methodology.

Small-scale reflection 62 is another methodology promoted by the MathComp project. Its ultimate goal is to ease formal proofs by systematically dealing with as many bureaucratic steps as possible, by automated computation. For instance, as opposed to the style advocated by Coq's standard library, decidable predicates are systematically represented using computable boolean functions: comparison on integers is expressed as program, and to state that $a\le b$ one compares the output of this program run on $a$ and $b$ with $true$. In many cases, for example when $a$ and $b$ are values, one can prove or disprove the inequality by pure computation.

The MathComp library was consistently designed after uniform principles of software engineering. These principles range from simple ones, like naming conventions, to more advanced ones, like generic programming, resulting in a robust and reusable collection of formal mathematical components. This large body of formalized mathematics covers a broad panel of algebraic theories, including of course advanced topics of finite group theory, but also linear algebra, commutative algebra, Galois theory, and representation theory. We refer the interested reader to the online documentation of these libraries 84, which represent about 150,000 lines of code and include roughly 4,000 definitions and 13,000 theorems.

Topics not addressed by these libraries and that might be relevant to the present project include real analysis and differential equations. The most advanced work of formalization on these domains is available in the HOL-Light system 67, 69, 70, although some existing developments of interest 43, 76 are also available for Coq. Another aspect of the MathComp libraries that needs improvement, owing to the size of the data we manipulate, is the connection with efficient data structures and implementations, which only starts to be explored.

3.19 User interaction with the proof assistant

The user of a proof assistant describes the proof he wants to formalize in the system using a textual language. Depending on the peculiarities of the formal system and the applicative domain, different proof languages have been developed. Some proof assistants promote the use of a declarative language, when the Coq and Matita systems are more oriented toward a procedural style.

The development of the large, consistent body of MathComp libraries has prompted the need to design an alternative and coherent language extension for the Coq proof assistant 64, 63, enforcing the robustness of proof scripts to the numerous changes induced by code refactoring and enhancing the support for the methodology of small-scale reflection.

The development of large libraries is quite a novelty for the Coq system. In particular any long-term development process requires the iteration of many refactoring steps and very little support is provided by most proof assistants, with the notable exception of Mizar 81. For the Coq system, this is an active area of research.

4.1 Computer Algebra in Mathematics

Our expertise in computer algebra and complexity-driven design of algebraic algorithms has applications in various domains, including:

• combinatorics, especially the study of combinatorial walks,
• theoretical computer science, like by the study of automatic sequences,
• number theory, by the analysis of the nature of so-called periods.

5.1 Refounding the team: towards computer algebra, experimental mathematics, and interactions

The team has worked on its renewal and has presented a project for a new team, MATHEXP. This new team will develop and implement symbolic and semi-numerical computational methods to deal with special functions and numbers in experimental mathematics.

5.2 ERC project: 10,000 DIGITS

Lairez's ERC proposal has been retained for funding with a grant of roughly 1.4 million Euro. The project will focus on the foundations of transcendental methods in numerical nonlinear algebra.

5.3 David P. Robbins Prize

Alin Bostan, of the team, together with Irina Kurkova and Kilian Raschel, will receive the 2022 AMS David P. Robbins Prize for their paper “A human proof of Gessel's lattice path conjecture,” published in Transactions of the American Mathematical Society in 2017. The paper proves highly nontrivial enumeration results on a family of lattice paths known as Gessel walks.

5.4 Promotion

Alin Bostan was nominated “Directeur de Recherche” in 2021.

6.1 Algebraic algorithms on fundamental objects

6.2 Polynomial systems and geometry

6.3 Applications to special functions and number theory

6.4 Applications to combinatorics

6.5 Applications to probability

6.6 Diagonals

6.7 Proceedings of a conference on our topics

7.1 International initiatives

7.2 European initiatives

7.3 National initiatives

7.4 Regional initiatives

• Alin Bostan submitted a PCRI-ANR proposal EAGLE – “Efficient Algorithms for Guessing, Summation, and InequaLitiEs”. This is a bilateral ANR/FWF project between 2 computer algebra teams in France and 2 computer algebra teams in Austria. The Austrian co-leader is Manuel Kauers from Univ. Linz. The goal is to work together on four axes: structured and multivariate guessing, inequalities and D-finiteness, creative telescoping and applications in combinatorics, number theory and theoretical physics. The requested funding is of 770,000 euros in total.
• Alin Bostan is co-leader of the Amadeus (Campus France) bilateral project “Integer Sequences arising in Number Theory, Combinatorics and Physics” between France and Austria. The Austrian co-leader is Herwig Hauser (U. Vienna, Austria).

8.1 Promoting scientific activities

8.2 Teaching - Supervision - Juries

9.1 Major publications

• 1 inproceedingsA.Alexandre Benoit, A.Alin Bostan and J.Joris Van Der Hoeven. Quasi-optimal multiplication of linear differential operators.FOCS 2012 - IEEE 53rd Annual Symposium on Foundations of Computer ScienceNew Brunswick, United StatesIEEEOctober 2012, 524-530
  HALDOI
• 2 articleA.Alin Bostan, M.Mireille Bousquet-Mélou and S.Stephen Melczer. Counting walks with large steps in an orthant.Journal of the European Mathematical Society2020
  HAL
• 3 inproceedingsA.Alin Bostan, X.Xavier Caruso, G.Gilles Christol and P.Philippe Dumas. Fast Coefficient Computation for Algebraic Power Series in Positive Characteristic.ANTS-XIII - Thirteenth Algorithmic Number Theory Symposium2Proceedings of the Thirteenth Algorithmic Number Theory Symposium (ANTS--XIII)1Madison, United StatesMathematical Sciences PublishersJuly 2018, 119-135
  HALDOI
• 4 bookA.Alin Bostan, F.Frédéric Chyzak, M.Marc Giusti, R.Romain Lebreton, G.Grégoire Lecerf, B.Bruno Salvy and E.Eric Schost. Algorithmes Efficaces en Calcul Formel.Voir la page du livre à l'adresse https://hal.archives-ouvertes.fr/AECF/published by the Authors2017
  HAL
• 5 inproceedingsA.Alin Bostan, F.Frédéric Chyzak, P.Pierre Lairez and B.Bruno Salvy. Generalized Hermite Reduction, Creative Telescoping and Definite Integration of D-Finite Functions.ISSAC 2018 - International Symposium on Symbolic and Algebraic ComputationNew York, United StatesJuly 2018, 1-8
  HALDOI
• 6 articleA.Alin Bostan, F.Frédéric Chyzak, M.Mark Van Hoeij, M.Manuel Kauers and L.Lucien Pech. Hypergeometric Expressions for Generating Functions of Walks with Small Steps in the Quarter Plane.European Journal of Combinatorics612017, 242-275
  HALDOI
• 7 articleP.Peter Bürgisser, F.Felipe Cucker and P.Pierre Lairez. Computing the Homology of Basic Semialgebraic Sets in Weak Exponential Time.Journal of the ACM (JACM)661December 2018, 1-30
  HALDOI
• 8 articleF.Frédéric Chyzak, T.Thomas Dreyfus, P.Philippe Dumas and M.Marc Mezzarobba. Computing solutions of linear Mahler equations.Mathematics of Computation87July 2018, 2977-3021
  HALDOI
• 9 inproceedingsF.Frédéric Chyzak, A.Assia Mahboubi, T.Thomas Sibut-Pinote and E.Enrico Tassi. A Computer-Algebra-Based Formal Proof of the Irrationality of $$(3).ITP - 5th International Conference on Interactive Theorem ProvingVienna, Austria2014
  HAL
• 10 articleP.Pierre Lairez. Computing periods of rational integrals.Mathematics of Computation85November 2016, 1719-1752
  HALDOI

9.2 Publications of the year

9.3 Cited publications

• 37 articleY.Y. Abdelaziz, C.C. Koutschan and J.-M.J.-M. Maillard. On Christol's conjecture.J. Phys. A53202020, 205201, 16 pagesURL: https://doi.org/10.1088/1751-8121/ab82dc
  DOIback to textback to text
• 38 bookM.Milton AbramowitzI. A.Irene A. StegunHandbook of mathematical functions with formulas, graphs, and mathematical tables.Reprint of the 1972 editionNew YorkDover1992, xiv+1046
  back to textback to textback to text
• 39 inproceedingsM.Michaël Armand, B.Benjamin Grégoire, A.Arnaud Spiwack and L.Laurent Théry. Extending Coq with Imperative Features and its Application to SAT Verication.Interactive Theorem Proving, international Conference, ITP 2010, Edinburgh, Scotland, July 11--14, 2010, ProceedingsLecture Notes in Computer ScienceSpringer2010
  back to text
• 40 articleB.B. Beckermann and G.G. Labahn. A uniform approach for the fast computation of matrix-type Padé approximants.SIAM J. Matrix Anal. Appl.1531994, 804--823
  back to text
• 41 inproceedingsA.Alexandre Benoit, F.Frédéric Chyzak, A.Alexis Darrasse, S.Stefan Gerhold, M.Marc Mezzarobba and B.Bruno Salvy. The Dynamic Dictionary of Mathematical Functions (DDMF).The Third International Congress on Mathematical Software (ICMS 2010)6327Lecture Notes in Computer Science2010, 35--41
  back to textback to text
• 42 inproceedingsM.Mathieu Boespflug, M.Maxime Dénès and B.Benjamin Grégoire. Full reduction at full throttle.First International Conference on Certified Programs and Proofs, Taiwan, December 7--9Lecture Notes in Computer ScienceSpringer2011
  back to text
• 43 incollectionS.Sylvie Boldo, C.Catherine Lelay and G.Guillaume Melquiond. Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives.Certified Programs and Proofs7679Lecture Notes in Computer ScienceSpringer Berlin Heidelberg2012, 289-304URL: http://dx.doi.org/10.1007/978-3-642-35308-6_22
  back to text
• 44 inproceedingsS.Sylvie Boldo and G.Guillaume Melquiond. Flocq: A Unified Library for Proving Floating-point Algorithms in Coq.Proceedings of the 20th IEEE Symposium on Computer ArithmeticTübingen, GermanyJuly 2011, 243--252
  back to text
• 45 inproceedingsA.Alin Bostan. Algorithmes rapides pour les polynômes, séries formelles et matrices.Actes des Journées Nationales de Calcul FormelLes cours du CIRM, tome 1, numéro 2Luminy, France2010, 75--262URL: http://ccirm.cedram.org:80/ccirm-bin/fitem?id=CCIRM_2010__1_2_75_0
  back to text
• 46 articleA.Alin Bostan, S.S. Boukraa, S.S. Hassani, J.-M.J.-M. Maillard, J.-A.Jacques-Arthur Weil and N.N. Zenine. Globally nilpotent differential operators and the square Ising model.J. Phys. A: Math. Theor.42122009, 50URL: http://dx.doi.org/10.1088/1751-8113/42/12/125206
  back to text
• 47 inproceedingsA.Alin Bostan, S.Shaoshi Chen, F.Frédéric Chyzak and Z.Ziming Li. Complexity of creative telescoping for bivariate rational functions.ISSAC'10: Proceedings of the 2010 International Symposium on Symbolic and Algebraic ComputationNew York, NY, USAACM2010, 203--210URL: http://doi.acm.org/10.1145/1837934.1837975
  back to text
• 48 articleA.Alin Bostan, F.Frédéric Chyzak, M.Mark van Hoeij and L.Lucien Pech. Explicit formula for the generating series of diagonal 3D rook paths.Sém. Loth. Comb.B66a2011, 27URL: http://www.emis.de/journals/SLC/wpapers/s66bochhope.html
  back to text
• 49 inproceedingsA.Alin Bostan, F.Frédéric Chyzak, G.Grégoire Lecerf, B.Bruno Salvy and É.Éric Schost. Differential equations for algebraic functions.ISSAC'07: Proceedings of the 2007 international symposium on Symbolic and algebraic computationACM Press2007, 25--32URL: http://dx.doi.org/10.1145/1277548.1277553
  back to text
• 50 articleA.Alin Bostan and M.Manuel Kauers. The complete generating function for Gessel walks is algebraic.Proceedings of the American Mathematical Society1389With an appendix by Mark van Hoeij2010, 3063--3078
  back to textback to text
• 51 articleF.Frédéric Chyzak. An extension of Zeilberger's fast algorithm to general holonomic functions.Discrete Math.2171-3Formal power series and algebraic combinatorics (Vienna, 1997)2000, 115--134
  back to text
• 52 inproceedingsF.Frédéric Chyzak, M.Manuel Kauers and B.Bruno Salvy. A Non-Holonomic Systems Approach to Special Function Identities.ISSAC'09: Proceedings of the Twenty-Second International Symposium on Symbolic and Algebraic Computation2009, 111--118URL: http://dx.doi.org/10.1145/1576702.1576720
  back to text
• 53 articleF.Frédéric Chyzak and B.Bruno Salvy. Non-commutative elimination in Ore algebras proves multivariate identities.J. Symbolic Comput.2621998, 187--227
  back to textback to text
• 54 miscComputer Algebra Errors.URL: http://mathoverflow.net/questions/11517/computer-algebra-errors
  back to text
• 55 articleT.Thierry Coquand and G. P.Gérard P. Huet. The Calculus of Constructions.Inf. Comput.762/31988, 95-120URL: http://dx.doi.org/10.1016/0890-5401(88)90005-3
  back to text
• 56 inproceedingsT.Thierry Coquand and C.Christine Paulin-Mohring. Inductively defined types.Proceedings of Colog'88417Lecture Notes in Computer ScienceSpringer-Verlag1990
  back to text
• 57 articleD.David Delahaye and M.Micaela Mayero. Dealing with algebraic expressions over a field in Coq using Maple.J. Symbolic Comput.395Special issue on the integration of automated reasoning and computer algebra systems2005, 569--592URL: http://dx.doi.org/10.1016/j.jsc.2004.12.004
  back to text
• 58 bookG.Guy Fayolle, R.Roudolf Iasnogorodski and V.Vadim Malyshev. Random walks in the quarter plane.Springer International Publishing2017
  DOIback to textback to textback to text
• 59 inproceedingsF.François Garillot, G.Georges Gonthier, A.Assia Mahboubi and L.Laurence Rideau. Packaging Mathematical Structures.Theorem Proving in Higher-Order Logics5674Lecture Notes in Computer ScienceSpringer2009, 327--342
  back to textback to text
• 60 bookJ.J. von zur Gathen and J.J. Gerhard. Modern computer algebra.New YorkCambridge University Press2003, xiv+785
  back to text
• 61 articleG.Georges Gonthier. Formal proofs---the four-colour theorem.Notices of the AMS55112008, 1382-1393
  back to text
• 62 articleG.Georges Gonthier and A.Assia Mahboubi. An introduction to small scale reflection in Coq.Journal of Formalized Reasoning322010, 95--152
  back to text
• 63 techreportG.Georges Gonthier, A.Assia Mahboubi and E.Enrico Tassi. A Small Scale Reflection Extension for the Coq system.RR-6455INRIA2008
  HALback to text
• 64 inproceedingsG.Georges Gonthier and E.Enrico Tassi. A language of patterns for subterm selection.ITP7406LNCS2012, 361--376
  back to text
• 65 inproceedingsB.Benjamin Grégoire and A.Assia Mahboubi. Proving Equalities in a Commutative Ring Done Right in Coq.Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings3603Lecture Notes in Computer ScienceSpringer2005, 98--113
  back to textback to text
• 66 articleT.Thomas Hales. Formal proof.Notices of the AMS55112008, 1370-1380
  back to textback to text
• 67 inproceedingsJ.John Harrison. A HOL Theory of Euclidean space.Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 20053603Lecture Notes in Computer ScienceOxford, UKSpringer-Verlag2005, 114--129
  back to text
• 68 inproceedingsJ.John Harrison. A Machine-Checked Theory of Floating Point Arithmetic.Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs'991690Lecture Notes in Computer ScienceNice, FranceSpringer-Verlag1999, 113--130
  back to text
• 69 articleJ.John Harrison. Formalizing an analytic proof of the prime number theorem.Journal of Automated Reasoning43Dedicated to Mike Gordon on the occasion of his 60th birthday2009, 243--261
  back to text
• 70 bookJ.John Harrison. Theorem proving with the real numbers.CPHC/BCS distinguished dissertationsSpringer1998
  back to text
• 71 articleJ.John Harrison and L.Laurent Théry. A Skeptic's Approach to Combining HOL and Maple.J. Autom. Reason.213December 1998, 279--294URL: http://dx.doi.org/10.1023/A:1006023127567
  back to text
• 72 miscF.Fredrik Johansson. Another Mathematica bug.2009, URL: http://fredrik-j.blogspot.fr/2009/07/another-mathematica-bug.html
  back to text
• 73 articleC.Christoph Koutschan. A fast approach to creative telescoping.Math. Comput. Sci.42-32010, 259--266URL: http://dx.doi.org/10.1007/s11786-010-0055-0
  DOIback to text
• 74 articleA.Assia Mahboubi. Implementing the cylindrical algebraic decomposition within the Coq system.Mathematical Structures in Computer Science1712007, 99--127
  back to text
• 75 articleR.Roman Matuszewski and P.Piotr Rudnicki. Mizar: the first 30 years.Mechanized Mathematics and Its Applications42005
  back to text
• 76 phdthesisM.Micaela Mayero. Problèmes critiques et preuves formelles.Université Paris 132012
  back to text
• 77 incollectionM.Marc Mezzarobba. NumGfun: a package for numerical and analytic computation and D-finite functions.ISSAC 2010---Proceedings of the 2010 International Symposium on Symbolic and Algebraic ComputationNew YorkACM2010, 139--146URL: http://dx.doi.org/10.1145/1837934.1837965
  DOIback to text
• 78 bookF. W.Frank W. J. OlverD. W.Daniel W. LozierR. F.Ronald F. BoisvertC. W.Charles W. ClarkNIST Handbook of mathematical functions.Cambridge University Press2010
  back to textback to text
• 79 articleP.Peter Paule and M.Markus Schorn. A Mathematica version of Zeilberger's algorithm for proving binomial coefficient identities.J. Symbolic Comput.205-6Symbolic computation in combinatorics ${}_1$ (Ithaca, NY, 1993)1995, 673--698URL: http://dx.doi.org/10.1006/jsco.1995.1071
  DOIback to text
• 80 miscB.Bent Petersen. Maple.
  back to text
• 81 inproceedingsP.Piotr Rudnicki and A.Andrzej Trybulec. On the Integrity of a Repository of Formalized Mathematics.Proceedings of the Second International Conference on Mathematical Knowledge ManagementMKM '03London, UKSpringer-Verlag2003, 162--174URL: http://dl.acm.org/citation.cfm?id=648071.748518
  back to text
• 82 articleB.Bruno Salvy and P.Paul Zimmermann. Gfun: a Maple package for the manipulation of generating and holonomic functions in one variable.ACM Trans. Math. Software2021994, 163--177
  back to text
• 83 bookN. J.N. J. A. Sloane and S.S. Plouffe. The Encyclopedia of Integer Sequences.Academic Press, San Diego1995
  back to text
• 84 miscT. M.The Mathematical Component Team. A Formalization of the Odd Order Theorem using the Coq proof assistant.2012, URL: http://www.msr-inria.fr/projects/mathematical-components/
  back to text
• 85 miscT. C.The Coq Development Team. The Coq Proof Assistant: Reference Manual.URL: http://coq.inria.fr/doc/
  back to textback to textback to text
• 86 articleL.Laurent Théry. A Machine-Checked Implementation of Buchberger's Algorithm.J. Autom. Reasoning2622001, 107-137URL: http://dx.doi.org/10.1023/A:1026518331905
  back to text
• 87 mastersthesisK.Kurt Wegschaider. Computer generated proofs of binomial multi-sum identities.MA ThesisRISC, J. Kepler UniversityMay 1997, 99
  back to text
• 88 bookS.Stephen Wolfram. Mathematica: A system for doing mathematics by computer (2nd ed.).Addison-Wesley1992
  back to text
• 89 miscT.Thomas Yu and J.Jingmin Chen. On the Uniqueness of Clifford Torus with Prescribed Isoperimetric Ratio.Technical Report ://arxiv.org/abs/2003.13116arXiv:2003.13116 [math.DG]2020
  back to text
• 90 articleD.Doron Zeilberger. A holonomic systems approach to special functions identities.J. Comput. Appl. Math.3231990, 321--368
  back to textback to text
• 91 miscD.Doron Zeilberger. Opinion 94: The Human Obsession With “Formal Proofs” is a Waste of the Computer's Time, and, Even More Regretfully, of Humans' Time.2009, URL: http://www.math.rutgers.edu/~zeilberg/Opinion94.html
  back to text
• 92 articleD.Doron Zeilberger. The method of creative telescoping.J. Symbolic Comput.1131991, 195--204
  back to text