Le séminaire des doctorants se propose de fournir aux doctorants une occasion de s'ouvrir aux autres domaines des mathématiques que le leur. A chaque séance, un intervenant réalise un exposé sur un fait standard de leur domaine d'étude, de niveau adapté à l'ensemble des doctorants.

Un anneau de polynômes est-il l'ensemble des suites à support fini ou l'ensemble des fonctions polynomiales ? 

Mon lemme de topologie est vrai dans les espaces métriques, les espaces compacts ou même les groupes topologiques, mais je ne souhaite pas le démontrer plusieurs fois. 

Je souhaite travailler avec des fonctions méromorphes, et pourtant, j'ai encore du mal à écrire rigoureusement toutes les conditions de la définition. 

Derrière ces exemples se cache une dure réalité : 
- Nos preuves sont très vulnérables à une légère modification anodine des pages précédentes. 
- Nous devons souvent refaire des preuves très similaires en raison d'hypothèses légèrement différentes. 
- Nos preuves doivent tenir compte de la manière dont nous avons démontré certains lemmes (et pas seulement des lemmes). 

Ce sont précisément les problèmes que certains paradigmes de programmation nous permettent d'éviter. Cela est particulièrement utile pour expliquer les mathématiques à un assistant de preuve, mais nous verrons que la mise en œuvre de ces paradigmes sur nos trois exemples peut changer la façon dont nous faisons des mathématiques « sur papier ».

-------

The PhD students seminar aims to provide PhD students with an opportunity to explore other areas of mathematics beyond their own. At each session, a speaker gives a presentation on a standard topic in their field of study, at a level suitable for all doctoral students.

What can mathematicians learn from developers? 

Is a ring of polynomials the set of sequences with finite support or the set of polynomial functions? 

My topology lemma is true in metric spaces, compact spaces, or even topological groups, but I don't want to prove it multiple times. 

I want to work with meromorphic functions, and yet I still struggle to rigorously write all the conditions of the definition. 

Behind these examples lies a harsh reality: 

- Our proofs are very vulnerable to a small, innocuous modification of previous pages. 
- We often have to redo very similar proofs because of slightly different assumptions. 
- Our proofs must take into account how we proved certain lemmas (and not just lemmas). 

These are precisely the problems that certain programming paradigms allow us to avoid. This is particularly useful when explaining math to a proof assistant, but we will see that implementing these paradigms on our three examples can change the way we do « pen-and-paper » mathematics.