1.9 KiB
Session 1
- Le jeudi 15/02/2024
- Présentations de 18h30 à 19h30, la suite tant qu'il restera du monde
- Campus Panthéon, la salle n'est pas encore déterminée
Présentations
- Présentation des SIMI
- Julien Marquet-Wagner -- Coalgèbres Terminales
- Gabriel Doriath Döhler -- Présentation de Lean
SIMI
En SIMI, Sessions Informelles Maths-Info, le principe est d'avoir une ou deux présentations chaque semaine, et d'avoir un repas ensuite. L'idée vient de nous (Gabriel et Julien). On essaye de faire deux choses en même temps : d'un côté, on aime bien avoir des projets personnels et on veut se donner un cadre qui nous motiverait pour les réaliser, et d'un autre, on veut avoir un endroit qui rejoint le DI et le DMA dans une bonne ambiance. Penser : le séminaire du DMA et le thé du DMA, par des normalien·ne·s dans une abiance de club du COF à la HackENS.
Nous avons choisi le thème des types coinductifs et de Lean 4 pour nous donner un cadre, l'idée étant de ne pas trop nous disperser tout en gardant un champ de possibilités assez large pour que chacun·e puisse s'amuser. Du point de vue mathématique, c'est un sujet qui s'étudie avec des outils catégoriques assez élémentaires. C'est parfait pour nous : c'est une rare occasion d'entrer dans les catégories sans avoir à étudier de maths très avancées, et la courbe d'apprentissage nous est favorable car on peut varier la difficulté entre le très abordable et le problème ouvert. Du côté informatique, Lean 4 est à la fois un outil que nous trouvons très agréable à explorer, et une communauté très active en pleine expansion. Lean 4 étant à la fois un assistant à la preuve et un langage de programmation, les thèmes informatiques varient de la pure théorie des types à la compilation.
En d'autres termes, que vous soyez mathématicien·ne ou informaticien·ne, il y en a pour tout le monde.