Montreal.IA

06/06/2026

Les co-mathématiciens IA ne naîtront pas seulement de prouveurs plus puissants.

Ils naîtront de systèmes capables de préserver une preuve sur la durée.

Nouveau papier de Yuanhe Zhang, Yuekai Sun, Taiji Suzuki, Jason D. Lee et Fanghui Liu :

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

Le problème n’est pas seulement de prouver un lemme difficile.

C’est de maintenir la fidélité mathématique d’un développement entier.

À l’échelle d’un article, l’autoformalisation échoue autrement :

les énoncés dérivent
les dépendances s’emmêlent
le contexte se dégrade
les réparations locales cassent des preuves lointaines
un lemme formellement correct peut devenir mathématiquement hors sujet

Le vrai goulot d’étranglement est donc la durabilité agentique.

LeanMarathon traite la formalisation Lean comme un système d’ingénierie de la vérité mathématique.

Son abstraction centrale : un blueprint évolutif.

Un fichier Lean qui sert à la fois de squelette formel, graphe de preuve en langage naturel, DAG de dépendances et système de référence partagé.

Quatre agents à périmètre contractuel travaillent dessus :

Blueprinter — construit le squelette Lean
Target Reviewer — vérifie la fidélité aux théorèmes visés
Worker — prouve les nœuds locaux
Refiner — répare les défauts multi-nœuds

L’orchestrateur opère en deux temps :

d’abord stabiliser les énoncés par r***e adversariale,
puis décharger le DAG de preuve depuis les feuilles dynamiques, en parallèle, avec validation CI.

Le geste clé :

ne pas faire confiance à un agent monolithique pour tout retenir.

Limiter le périmètre.
Externaliser l’état.
Vérifier déterministiquement.
Faire de la CI l’autorité de merge.
Rendre les erreurs locales, récupérables et non contagieuses.

En Lean, “sorry” est le placeholder qui permet à une preuve incomplète de passer.

LeanMarathon rapporte avoir formalisé les sept théorèmes cibles de deux articles récents couvrant quatre problèmes d’Erdős, sans aucun sorry, avec 258 lemmes et théorèmes prouvés sur trois runs autonomes.

Ce n’est pas seulement du proof search.

C’est du long-horizon proof engineering.

Et la leçon dépasse les mathématiques :

la fiabilité à l’échelle est un problème de harness.

Le futur de l’IA mathématique ne demandera pas seulement des modèles plus forts.

Il demandera des systèmes durables qui préservent l’intention, les dépendances et la vérification sur de longues chaînes de raisonnement.

Crédit complet aux auteurs :
Yuanhe Zhang, Yuekai Sun, Taiji Suzuki, Jason D. Lee, Fanghui Liu.

Paper :
https://arxiv.org/abs/2606.05400

Code :
https://github.com/YuanheZ/LeanMarathon

J’attache la première page, car l’abstract mérite une lecture attentive.

La prochaine frontière n’est pas une IA qui écrit des preuves plausibles.

C’est une IA dont le travail mathématique survit au marathon.

06/03/2026

Le progrès en IA n’est pas un modèle.

C’est une machine capable d’améliorer les modèles, encore et encore.

Le nouveau rapport technique de Microsoft AI pose une thèse très forte :

MAI-Thinking-1: Building a Hill-Climbing Machine

Ce n’est pas seulement une sortie de modèle.

C’est une vision institutionnelle de la recherche frontier AI comme boucle d’optimisation systémique.

MAI-Thinking-1 est un modèle de raisonnement MoE entraîné from scratch par Microsoft AI : 35B paramètres actifs, environ 1T paramètres au total.

Mais le point central n’est pas seulement le benchmark.

Le point central est la machine qui produit le benchmark.

Microsoft décrit le développement de modèles comme un hill climb intégré :

pipelines de données
échelles d’architecture
ablations de pré-entraînement
co-design infrastructurel
recettes de reinforcement learning
suites d’évaluation
sécurité
red teaming
efficacité de déploiement

Optimisés ensemble.

C’est la leçon institutionnelle.

À l’échelle frontier, la performance ne vient pas d’une seule astuce brillante.

Elle vient d’un système reproductible qui transforme l’évidence empirique en amélioration continue.

Trois principes structurent le rapport :

Les capacités doivent être apprises, pas héritées.

La simplicité est durable.

La rigueur scientifique évite les raccourcis.

C’est une position forte dans un champ saturé de distillation, de données synthétiques, de benchmark chasing et de recettes opaques.

MAI-Thinking-1 est entraîné from scratch, sans distillation depuis des modèles tiers, sur des données propres de niveau enterprise. Le rapport indique un pré-entraînement sur 30T tokens issus de sources humaines publiques et licenciées, suivi d’un mid-training, sans données synthétiques générées par modèles de langage pendant le pré-entraînement.

Puis vient la montée RL.

Le modèle part sans exposition préalable à des traces de raisonnement et apprend à raisonner via feedback de tâches, chaînes de pensée, interaction avec outils, préférences humaines et signaux de sécurité.

L’équipe entraîne des spécialistes pour :

raisonnement STEM
codage agentique et tool use
helpfulness et safety

Puis consolide ces capacités dans un modèle unique.

Les résultats rapportés sont sérieux :

52.8% sur SWE-Bench Pro
97.0% sur AIME 2025
94.5% sur AIME 2026
87.7% sur LiveCodeBench v6

Mais encore une fois, les chiffres ne sont pas toute l’histoire.

Le modèle est le produit visible.

La “hill-climbing machine” est l’actif profond.

Un score peut être dépassé.
Une recette peut vieillir.
Un modèle peut être imité.

Mais une organisation capable de faire tourner des ablations propres, améliorer son infrastructure, soutenir de longues montées RL, intégrer la sécurité, mesurer les échecs, et capitaliser l’apprentissage entre générations possède quelque chose de beaucoup plus difficile à copier :

un moteur de recherche et d’ingénierie.

C’est pourquoi ce rapport mérite une lecture attentive.

Il ne parle pas seulement de MAI-Thinking-1.

Il montre comment les organisations frontier AI deviennent elles-mêmes des systèmes d’optimisation.

Crédit complet à The Microsoft AI Team.

Rapport :
MAI-Thinking-1: Building a Hill-Climbing Machine
https://microsoft.ai/wp-content/uploads/2026/06/main_20260602_2.pdf

J’attache la première page, car la Figure 1 capture parfaitement la thèse : une amélioration RL soutenue comme ascension.

Le futur de l’IA n’appartiendra peut-être pas au laboratoire avec un seul modèle brillant.

Il appartiendra à celui qui possède la meilleure machine de hill-climbing.

05/27/2026

Les modèles de langage n’ont peut-être pas besoin d’un contexte infini.

Ils ont peut-être besoin de sommeil.

Un papier fascinant de Sangyun Lee, Sean McLeish, Tom Goldstein et Giulia Fanti propose une idée rare : à la fois techniquement précise, biologiquement résonnante, et potentiellement structurante pour l’IA long-horizon.

Language Models Need Sleep

Le problème est subtil.

Les Transformers gardent le contexte récent dans un KV cache, mais l’attention devient coûteuse quand la séquence s’allonge.

Les architectures hybrides SSM-attention promettent une mémoire plus compacte via des “fast weights”.

Mais le papier insiste sur une distinction cruciale :

mémoire scalable ≠ raisonnement scalable.

Un modèle peut stocker du contexte évincé sans être capable de le transformer en état utile pour raisonner plus t**d.

C’est là que l’idée de “sleep” devient intéressante.

Quand la fenêtre de contexte se remplit, le modèle entre dans une phase de consolidation hors ligne.

Il relit le contexte accumulé pendant N passes récurrentes, met à jour des fast weights persistants dans ses blocs SSM via une règle locale apprise, puis efface le KV cache.

Ensuite, pendant l’inférence “éveillée”, la prédiction reste single-pass.

Le coût computationnel supplémentaire est payé pendant le sommeil, pas au moment de répondre.

C’est le geste architectural :

attention pour l’accès fidèle au contexte récent

fast weights pour la mémoire compressée à long terme

sommeil pour transformer cette mémoire en état exploitable

L’analogie biologique n’est pas décorative.

Chez l’animal, le sommeil est associé à la réactivation et à la consolidation de souvenirs courts en structures plus durables.

Ici, le modèle consolide le contexte évincé dans ses poids rapides avant de se réveiller et de continuer.

Le papier teste cette idée sur des tâches synthétiques contrôlées, comme Rule 110 et la récupération multi-hop Depo, puis sur GSM-Infinite, une tâche de raisonnement mathématique plus réaliste.

Résultat : augmenter la durée du sommeil améliore les performances, avec les gains les plus nets sur les exemples qui demandent un raisonnement plus profond.

La leçon profonde :

le long contexte ne consiste pas seulement à conserver plus de tokens.

Il faut aussi allouer assez de calcul pour métaboliser ce contexte.

Un cache statique se souvient.

Un modèle qui dort réorganise.

Si cette direction tient, les futurs agents ne fonctionneront peut-être pas dans un état d’éveil continu, absorbant indéfiniment du contexte.

Ils alterneront entre interaction et consolidation.

Lire.
Dormir.
Compresser.
Raisonner.
Se réveiller.

Crédit complet aux auteurs :
Sangyun Lee, Sean McLeish, Tom Goldstein, Giulia Fanti.

Paper :
Language Models Need Sleep
https://arxiv.org/abs/2605.26099

J’attache la première page, car l’abstract mérite vraiment d’être lu attentivement.

Le futur de l’IA long-horizon ne sera peut-être pas l’attention infinie.

Ce sera peut-être des modèles qui savent quand dormir.

05/24/2026

⚜️✨ Archive du dossier public

Vincent Boucher chez Liza Frulla à Radio-Canada — une entr***e de début de parcours sur l’éducation, l’apprentissage, la discipline, la volonté et la formation d’une vision à long terme.

De la reconstruction personnelle à l’intelligence publique.
Des méthodes d’apprentissage à l’ère AI-first.

Regarder : https://www.youtube.com/watch?v=pMyxMN7FQxU

Vincent Boucher on Liza Frulla at Radio-Canada — an early public-re...

05/19/2026

MONTREAL.IA | Intelligence Artificielle Montréal

Intelligence publique pour l’ère AGI-first.

Bienvenue sur la Page francophone renouvelée de MONTREAL.AI.

MONTREAL.IA est la couche francophone d’intelligence publique et de provenance de l’écosystème : identité, travail, preuve, règlement, mémoire et gouvernance pour l’époque où l’intelligence machine devient infrastructure stratégique.

Cette Page existe pour les développements IA sérieux, l’IA de frontière, l’AGI, les agents autonomes, AI Debate, l'IA souveraine, la recherche publique, le travail machine, la mémoire institutionnelle, les ressources médias et les idées à fort impact qui façonnent l’ère AGI-first.

Identité.
Travail.
Preuve.
Règlement.
Mémoire.
Gouvernance.

Pas d’autonomie sans autorité.
Gouvernance avant l’échelle récursive.
Identité avant l’échelle.
Preuve avant règlement.

Site officiel :
https://montreal.ai

Dossier public :
https://montrealai.github.io/

Surface d’autorité MONTREAL.AI :
https://www.vincentboucher.com/montreal-ai/

QUEBEC.AI :
https://quebec.ai

05/12/2026

QUEBEC.AI publie le Manifeste souverain / Sovereign Manifesto.

⚜️ Un Québec qui ne loue pas son avenir, mais qui le construit.

⚜️ A Québec that does not rent its future, but builds it.

Lire le document officiel / Read the official document: https://quebecai.github.io/sovereignmanifesto/

05/11/2026

La souveraineté, à l’ère de l’intelligence artificielle, est la capacité de ne pas subir l’intelligence des autres.

C’est la capacité de bâtir la nôtre.

De la gouverner.
De la sécuriser.
De la coordonner.
De la mettre au service des entreprises, des institutions, de la langue, de la culture, de la prospérité et de l’avenir.

QUEBEC.AI porte cette ambition au niveau de l’entreprise.

Transformer les entreprises prospères en organisations AI‑First.

Transformer le travail en preuve.
Transformer la preuve en confiance.
Transformer la confiance en capacité.
Transformer la capacité en puissance qui se renforce.

Voilà le sens du Manifeste souverain.