Actualités
Please, don't automate science! (Togelius Blog, 2025-12-08)
Early science acceleration experiments with GPT-5 (OpenAI, 2025-11-20)
Google Scholar Labs : AI powered scholar search (Google, 2025-11-18)
Lancement de Gemini 3 (service LLM grand public de Google, 2025-11-18)
Annals of Formalized Mathematics : un nouvel épi-journal dédié à la formalisation (CNRS, 2025-11-17)
Journée AI4Maths organisée par les sociétés savantes SFdS, SMAI, SMF (Institut Henri Poincaré, 2025-11-18)
Google DeepMind joins forces with five major institutions to wage war on a century-old problem with AI. (2025-10-30)
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
Projet ERC FRESCO: Fast and Reliable Symbolic Computation
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)
Expérimentation avec AlphaEvolve
Mathematical exploration and discovery at scale : (
post de blog de Terry Tao du 05/11/2025
et
papier arXiv du 03/11/2025
)