Quand l'IA démontre des théorèmes : produire du vrai suffit-il ?

Math & IA

Ou pourquoi le discernement reste la compétence la plus humaine — et la plus précieuse à transmettre à nos enfants.

Une idée qui n'est plus de la science-fiction

Imaginez une intelligence artificielle qui ne se contente plus de répondre à nos questions, mais qui étend elle-même le champ des connaissances humaines. En mathématiques, ce scénario est en train de devenir réalité.

Le secret ? Des outils appelés assistants de preuve, dont le plus connu s'appelle Lean. Un assistant de preuve est un logiciel qui vérifie un raisonnement mathématique ligne par ligne, avec une rigueur absolue. Aucune étape ne peut être sautée, aucune approximation n'est tolérée. Si la démonstration passe la vérification, elle est logiquement correcte — point final.

Autour de Lean s'est construite Mathlib, une immense bibliothèque collaborative qui rassemble des dizaines de milliers de théorèmes déjà formalisés. C'est un peu le Wikipédia des mathématiques vérifiées : chaque brique a été contrôlée par la machine, et chacune peut servir de fondation pour construire la suivante.

Voici où l'IA entre en scène : un modèle d'intelligence artificielle peut désormais proposer un théorème, en rédiger la démonstration formelle, et soumettre le tout à Lean. Si la vérification passe, nous obtenons une vérité mathématique nouvelle, certifiée par la machine. Pas une hallucination plausible, pas une réponse « probablement correcte » : une preuve, au sens le plus strict du terme.

Les progrès récents des IA sur des problèmes de niveau olympiades internationales de mathématiques montrent que cette capacité n'est plus théorique. Nous entrons dans une ère où la machine peut réellement contribuer à la production de connaissances mathématiques.

Mais alors, une question dérangeante

Et c'est ici que la réflexion devient vraiment intéressante.

Produire quelque chose de vrai, est-ce suffisant ?

Car voici un secret que tout mathématicien connaît : il existe une infinité de théorèmes vrais... et parfaitement inintéressants. On peut démontrer que 7 845 213 + 1 est un nombre pair ou impair. C'est vrai. C'est vérifiable. Et cela n'apprend rien à personne.

Une IA capable de générer des milliers de théorèmes valides par jour produirait essentiellement du bruit. Des vérités, oui — mais des vérités qui n'éclairent rien, ne connectent rien, n'ouvrent aucune porte.

Les grands mathématiciens ne se distinguent pas d'abord par leur capacité à démontrer. Ils se distinguent par leur intuition de ce qui mérite d'être démontré. Henri Poincaré parlait de ce sens de l'élégance mathématique : cette capacité presque esthétique à reconnaître la beauté d'une idée avant même de l'avoir prouvée, à sentir qu'un chemin mène quelque part alors qu'un autre s'enlise.

En mathématiques comme ailleurs, la validité ne suffit pas. Il faut du sens, de l'intérêt, de la beauté, du discernement.

Le vrai défi de l'IA n'est peut-être pas celui qu'on croit

On débat beaucoup de la capacité des IA à générer des idées nouvelles. Mais le débat le plus profond est peut-être ailleurs : une IA peut-elle apprendre à reconnaître les idées qui valent la peine d'être explorées ?

Le goût, le jugement, le sens de la pertinence — ces qualités se construisent dans une expérience du monde, une histoire, une culture, des échecs et des émerveillements. Peut-on les encoder ? Peut-on les apprendre à partir de données ? La question reste ouverte, et elle est passionnante.

Ce qui est certain, c'est que dans un monde où produire du contenu valide devient trivial — du code qui compile, des textes bien formés, des théorèmes vérifiés — la valeur se déplace. Elle se déplace vers celles et ceux qui savent choisir, hiérarchiser, discerner.

Ce que cela change pour nos enfants

C'est ici que cette réflexion, en apparence très abstraite, rejoint directement ma pratique quotidienne à Codeacademy123.

Quand un enfant de 8 ans utilise un outil d'IA pour générer du code, la question n'est plus « le code fonctionne-t-il ? » — l'outil s'en charge de mieux en mieux. Les vraies questions deviennent : est-ce que ce projet est intéressant ? Est-ce que cette solution est élégante ? Est-ce que cette idée mérite qu'on y passe l'après-midi ?

Concrètement, dans nos ateliers, cela se traduit ainsi :

• Nous demandons aux enfants de formuler leur vision avant de produire : qu'est-ce que tu veux créer, et pourquoi est-ce que ça t'intéresse ?

• Nous comparons plusieurs solutions à un même problème et nous discutons de celle qui est la plus claire, la plus simple, la plus belle — pas seulement de celle qui marche.

• Nous apprenons à critiquer les productions de l'IA : ce que la machine propose est un point de départ, jamais un verdict.

La technique s'apprend. Les outils évoluent — Scratch aujourd'hui, autre chose demain. Mais le jugement, le goût, le discernement : ça se cultive lentement, par la pratique, la discussion, la confrontation à de vrais choix. Et ça ne se délègue pas à une machine.

En guise de conclusion (provisoire)

Peut-être qu'un jour, une IA développera quelque chose qui ressemble au « goût » mathématique de Poincaré. Peut-être pas. Mais en attendant, une chose est sûre : former des enfants capables de discerner ce qui a de la valeur — dans les idées, dans le code, dans les créations — n'a jamais été aussi important.

C'est le pari de Codeacademy123 depuis 2015 : former des créateurs, pas des consommateurs. Et à l'ère de l'IA, créer, c'est d'abord savoir choisir.

Et vous, pensez-vous qu'une machine puisse un jour développer le sens de la belle idée ? La discussion est ouverte — en commentaire ou lors de nos prochains ateliers.