Abstract
The second seminar was devoted to the uses in mathematical research of computers in general, and proof assistants (Coq, HOL, Mizar, etc.) in particular. Long employed as a support for experiments and an aid to intuition, computer calculation can also make a full-fledged contribution to the demonstration of major theorems. The speaker developed the example of Helfgott's proof of Goldbach's weak conjecture, which calls for numerical framings of integrals ; she and her co-authors were able to formally demonstrate these framings via interval arithmetic verified in Coq. However, the formalization " on machine " of the usual algebraic structures poses subtle problems, notably linked to " the typical ambiguity " between a structure and its supporting set. After the first successes, where computer assistance enabled the completion of lengthy demonstrations (Four-Color Theorem, Kepler's Conjecture), will we see a new style of mathematics emerge from the use of these assistants ?
