Table of Contents
Presse
Expériences
Évenements
Autres ressources
Presse
2026-04-13
The AI Revolution in Math Has Arrived (Konstantin Kakaes)
2026-02-18
Proof Assistants in the Age of AI (Leonardo de Moura)
2025-12-08
Please, don't automate science! (Togelius Blog)
2025
Google and OpenAI Get 2025 IMO Gold
2025-10-30
Google DeepMind joins forces with five major institutions to wage war on a century-old problem with AI
2026-11-18
Google Scholar Labs : AI powered scholar search
2025-11-17
Annals of Formalized Mathematics : un nouvel épi-journal dédié à la formalisation (CNRS)
Expériences
2026-04-07
Formalization of De Giorgi--Nash--Moser Theory in Lean (Scott Armstrong, Julia Kempe)
2026-03-27
Mathematical methods and human thought in the age of AI (Tanya Klowden, Terence Tao)
2025-11-20
Early science acceleration experiments with GPT-5 (OpenAI)
2025-05-31
A Lean companion to “Analysis I” (Terence Tao)
2025
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
2025-11
Mathematical exploration and discovery at scale (Alpha evolve, Terrence Tao)
2025-09
Mathematical research with GPT-5 : a Malliavin-Stein experiment (arXiv.2509.03065)
2025
Formal Proof of the Four Color Theorem (Georges Gonthier et communauté Coq)
Évenements
2026-06-29
Proof assistants for teaching (PAT) proof and proving (Orsay)
2026-02-16
Proof & Program - AI-Assisted Formal Mathematics (Sorbonne Université)
2025-11-18
Journée AI4Maths organisée par les sociétés savantes SFdS, SMAI, SMF (Institut Henri Poincaré)
2025-04-04
Journée IA & mathématiques : une thématique au cœur de la recherche (PSL)
Autres ressources
Lean Community Blog
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)
Projet MALINCA - Mathematicae Lingua Franca - Bridging the Linguistic Gap Between the Mathematician and the Machine
Projet ERC FRESCO: Fast and Reliable Symbolic Computation