Projet collectif pour faire communauté en région parisienne autour de l’informatisation des mathématiques :

• usage de l’apprentissage automatique (notamment par réseaux de neurones) pour faire des mathématiques : ChatGPT, Gemini, …
• usage de la formalisation des mathématiques et des assistants de preuve : Lean, Coq/Rocq, …
• usage de la combinaison des deux !

Le séminaire automath est bimestriel, soit une fois tous les deux mois, accessible, style colloquium :

• Séance de lancement !
  Vendredi 30 janvier 2026, 11h, salle Dussane
  École normale supérieure, 45 rue d’Ulm, Paris
  Marc Lelarge - Titre à préciser

Pour vous tenir informé, n’hésitez pas à vous inscrire à la liste de diffusion https://lists.ens.psl.eu/wws/info/automath

Djalil Chafaï, Julie Delon, Borjan Geshkovski, Amaury Hayat, Marc Lelarge, Frédéric Marbach, et Gabriel Peyré.

• Journée AI4Maths organisée par les sociétés savantes SFdS, SMAI, SMF (Institut Henri Poincaré, 2025-11-18)
• Séminaire de philosophie de la pratique des mathématiques de Tim Gowers au Collège de France
  • Formalisation en Lean : Search, Reason or Recombine? Paradigms for Scaling Formal Proving (Fabian Gloeckle, 2025-11-10
  • Formalisation en Coq
    • Le cinquième nombre Busy Beaver (Tristan Stérin, 2025-10-27)
• Journée IA & mathématiques : une thématique au cœur de la recherche (PSL, 2025-04-04)
• Projet Malinca - Mathematicae Lingua Franca - Bridging the Linguistic Gap Between the Mathematician and the Machine
• Google and OpenAI Get 2025 IMO Gold
• Exemple d'introduction de la formalisation dans l'enseignement des mathématiques
  • A Lean companion to “Analysis I” (Terry Tao, Fall 2025)
• Exemples d'articles faisant progresser les mathématiques
  • Formalisation avec Coq
    • Formal Proof of the Four Color Theorem (Georges Gonthier et communauté Coq)
  • Contrexemple à Erdös avec Lean+ChatGPT
    • Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof (Boris Alexeev, Dustin G. Mixon, 2025)
    • Simplification par la communauté Lean : follow-up
  • Amélioration d'un resultat d'analyse stochastique avec ChatGPT
    • Mathematical research with GPT-5 : a Malliavin-Stein experiment (arXiv.2509.03065)

Automath est un clin d’œil à Nicolaas Govert de Bruijn.