Certified and Symbolic-Numeric Computation

May 22 to 26, 2023

ENS de Lyon, site Descartes, room D2 034.

Organizers: N. Brisebarre, A. Mahboubi, D. Pous, B. Salvy

The last twenty years have seen the advent of computer-aided proofs in mathematics and this trend is getting more and more important. This workshop aims at discussing the trust issues raised by the rise of computational mathematics, with an emphasis on numerical methods.

A first source of interest for such certified computations comes from theoretical parts of mathematics, such as dynamical systems or number theory, where the need for formalized definitions, and for proofs that can be checked computationally, has brought a lot of attention to formal proof systems. A typical example, in analytic number theory, is the recent proof of the ternary Goldbach conjecture by Helfgott, where a key part was played by a recent library for ball arithmetic, which relies heavily on computer algebra; the ultimate correctness guarantee can be achieved with the use of a formal proof system. Another source of interest comes from areas where numerical safety is critical, such as in autonomous vehicles, drones, or robust space mission design. There also, first interesting results have been obtained.

Unfortunately, most of the time, the necessary certification or formal verification routines are not easily available (or do not even exist). This is partly due to the fact that this field is still fairly recent but, actually, the main reasons are that the related scientific issues are difficult: algorithms returning certified error bounds are often terribly inefficient; obtaining formally verified implementations using a proof assistant requires a lot of manpower, and good backbone libraries.

The workshop will combine talks on recent proofs of mathematical results, where some level of certified computation played a crucial role, with overviews of the state-of-the-art on fast and stable numerical computations on computations returning certified numerical results, i.e., where an error bound is part of the output; on formally verified implementations for performing the aforementioned computations. The aim is to bring together experts from computer algebra, computer arithmetic, certified analysis and formal proof systems and practitioners of certified proofs in various parts of mathematics, so that they can exchange and interact on those issues that are at the interface between their areas.

Contact: csnc2023@ens-lyon.fr



Code of Conduct