Time: Nov 10, 2020 18:30 India
Math and Informatics, ever more fruitful interactions.
College de France.
The relation between math and algorithmics is very old. In a sense, one can even argue that mathematics was created to show that some already known algorithms worked in all cases and not only on some examples. Church and Turing, creators of the lambda-calculus and computability theory were mathematicians. Informatics was really born later with the introduction of computers, for which mathematicians played an important role. In the 70's, computer algebra was developed, as well as the formal semantics of programming languages and automatic program analysis techniques. But the cooperation between both sciences has deepened quickly in the last 20 years, with mutual enrichment. We will show this with a variety of examples : the systematic development of randomized and probabilistic algorithms to handle massive data, the use of boolean satisfiability (SAT) systems to solve open problems in number theory, the development of powerful proof assistants for mechanizing large mathematical proofs using rich logics (Feit-Thompson theorem, Kepler conjectures), and finally, the use of the same tools to perform mathematical proofs of the correctness of safety-critical computerized system