Proofs and algorithms seminar: Patrick Massot on Wednesday 09 July 2025 at 10h30, "Formalisation de topologie différentielle avec Lean"

===== Seminar of the proofs and algorithms pole =====

Hello everybody,

For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Patrick Massot (Laboratoire de Mathématiques d'Orsay, Université Paris-Saclay), invited by the Cosynus team.

***** Wednesday 09 July 2025 at 10h30, room Henri Poincaré *****

Patrick Massot -- Formalisation de topologie différentielle avec Lean

La technique de l’intégration convexe de Gromov est une technique générale de construction en topologie différentielle. Elle permet par exemple de démontrer le paradoxal théorème du retournement de la sphère de Smale. Dans cet exposé j’expliquerai brièvement cette technique puis je discuterai des obstacles rencontrés lors de la formalisation de ce sujet dans l’assistant de preuve Lean.



The list of upcoming seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/

The calendar of seminars can be found at:
https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics

To unsubscribe from this mailing list visit:
https://sympa.lix.polytechnique.fr/lists/signoff/proofs-algorithms-seminar