Actualités
-
- 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)
- Exemple d'introduction de la formalisation dans l'enseignement des mathématiques
- Exemples d'articles faisant progresser les mathématiques
- Formalisation avec Coq
- Contrexemple à Erdös avec Lean+ChatGPT
- Simplification par la communauté Lean : follow-up
- Amélioration d'un resultat d'analyse stochastique avec ChatGPT
- 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)