Verified Computational Mathematics (T: 45min + Q: 15min)

Jun 15, 2022, 2:30 PM
Centre de conférences Marilyn et James Simons (Le Bois-Marie)

Centre de conférences Marilyn et James Simons

Le Bois-Marie

35, route de Chartres 91440 Bures-sur-Yvette




Computers are widely used as observation instruments for testing and refining conjectures, in a broad range of mathematical areas. They actually even substantiate actual proof steps in published proofs. In particular, a large class of computer proofs today involve symbolic computations, often produced by computer algebra systems. While these systems have become amazingly efficient, they also tend to exhibit awkward behaviors on seemingly innocuous queries. This talk will discuss the challenges raised by the formal verification of symbolic computation, and the potential of proof assistants based on dependent types.

Presentation materials

There are no materials yet.