Une IA peut proposer mille découvertes en une heure. Lesquelles sont vraies ?
Slean le vérifie automatiquement, avec la rigueur d’une mathématique, sur des simulés où l’on peut tout vérifier. C’est le juge des de recherche de Mutome.
Pas 0 · 11 voitures
Comment ça marche, en trois temps
Un monde dont on connaît les règles exactes
Prenons la route ci-dessus. Une voiture avance si la place devant est libre, sinon elle attend. Ces règles sont écrites une fois pour toutes, sans ambiguïté : c’est un exact.
Une IA propose une affirmation
Un observe le monde et avance une idée, par exemple une : une quantité qui ne changerait jamais.
« Le nombre de voitures ne change jamais. »
Slean la teste, puis la prouve ou la réfute
Slean cherche un . S’il en trouve un, l’affirmation est réfutée. Sinon, il faut une preuve pour toutes les routes possibles, et c’est le qui la contrôle.
Démontré : vrai pour toutes les routes
Réfuté : voici le cas où c’est faux
Ces mondes sont volontairement simples, pour que tout puisse être vérifié exactement. La science du monde réel est l’objectif de long terme, pas ce que Slean fait aujourd’hui.
Pourquoi « Slean » ?
Slean = Science + Lean
Lean est un langage de programmation et un assistant de preuve : un petit y vérifie chaque preuve. Avec Mathlib, sa bibliothèque partagée, c’est ce qui permet aujourd’hui à l’IA de faire de vrais progrès en mathématiques : une machine peut essayer des milliers de preuves, et seules les correctes sont acceptées.
Slean apporte cette vérification automatique et cette bibliothèque qui s’accumule à la découverte scientifique, en commençant par des mondes simulés où l’on peut tout vérifier. Les agents de Mutome s’en servent pour savoir ce qu’ils ont vraiment trouvé.
Nos inspirations : Lean, Physlib, Wolfram, Minimo et d’autresJouez : devinez la loi
Une minute. Choisissez ce qui ne change jamais sur la route, et regardez Slean le tester puis le prouver.
Pas 0 · 11 voitures
Sur cette route, qu’est-ce qui ne change jamais ?
Ce que le noyau de Lean a réellement vérifié
Voici la loi de la route, écrite pour Lean. Cliquez sur une partie pour savoir ce qu’elle veut dire. Le l’a acceptée : elle est vraie pour les routes de toutes les tailles.
:
Accepté par le noyau, pour toutes les tailles d’anneau
theorem trafficLe nom de l’affirmation : « trafic ».Conserved« … ne change jamais » : le total reste le même à chaque pas, sur des routes de toutes les tailles.(eca 184)Le monde : la règle 184, celle du trafic.(tableFn 2 [0, 1]) 1Ce qu’on compte : 0 pour une case vide, 1 pour une voiture. Le total, c’est le nombre de voitures.:=« et voici pourquoi » : la preuve commence.conserved_of_fluxCheckLa preuve par vérifications locales : si chaque petit morceau de route est en règle, la route entière l’est, quelle que soit sa taille.(tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1Le certificat : combien de voitures traversent chaque frontière entre deux cases, écrit dans la convention de Lean.(by decide +kernel)C’est l’ordinateur qui fait toutes les vérifications locales, pas nous, et le noyau de Lean contrôle le résultat.
Mutome explore. Slean vérifie.
Les deux projets vont ensemble. Mutome est un laboratoire de recherche autonome : ses agents essaient beaucoup de choses, c’est le hasard dans la découverte. Slean décide, sans appel, si ce qu’ils ont trouvé est vrai : c’est le déterminisme dans la vérification.
- Mutome
- Le hasard dans la découverte
- Slean
- Le déterminisme dans la vérification
- Un agent proposeUne loi, une structure ou une réfutation sur un monde exact.
- Slean vérifieLe noyau de Lean accepte le certificat, ou un contre-exemple réfute.
- La bibliothèque gardeChaque résultat devient un théorème réutilisable.
- La mesure noteContre des réponses cachées, face à des méthodes simples à coût égal.
Trois autres jeux
Chacun prend une ou deux minutes et montre une autre facette de Slean.
Premiers résultats
Nous avons lâché un d’IA dans des labos de 16 mondes inconnus, règles cachées, et comparé ce qu’il trouve à un programme de référence qui cherche méthodiquement. Même budget, mêmes commandes.
Découvertes acceptées selon les expériences dépensées
Voir les données
| Passage | Mises à jour de cellules | Découvertes acceptées |
|---|---|---|
| Référence scriptée, graine 7 | 199 748 | 88 |
| Agent Claude Sonnet, graine 7 | 888 | 90 |
| Référence scriptée, graine 11 | 199 802 | 93 |
| Agent Claude Sonnet, graine 11 | 1 277 | 98 |
Comment lire ce graphique
Chaque point est un passage complet dans un labo. Plus il est haut, plus il a trouvé de découvertes vraies. Plus il est à gauche, moins il a eu besoin d’expériences. L’agent (en vert) est en haut à gauche.
Lecture honnête
La boucle et la mesure fonctionnent : mondes inédits, réponses cachées, expériences comptées, et aucune affirmation fausse acceptée, de personne.
L’agent trouve un peu plus que la référence avec 150 à 225 fois moins d’expériences.
Mais ces mondes s’identifient en une seule expérience. Nous en avons donc construit de plus durs, où inférer une loi courte est la tâche : là, les leçons que l’agent a tirées de labos précédents ont amélioré ses résultats sur chaque graine inédite (+7 à +12). Un seul passage par graine : c’est encore une première mesure.
Toutes les mesures, y compris les négativesQuatre sortes de preuves
« Vrai » peut vouloir dire quatre choses différentes. Slean ne les mélange jamais : une loi démontrée dans un monde de cases n’est pas une loi de la nature.
| Sorte | Ce que cela veut dire | Exemple dans Slean |
|---|---|---|
| Démontré dans un monde | Un théorème Lean sur la définition exacte d’un monde. Vrai pour ce monde, sans condition. | Le trafic : le nombre de voitures est conservé pour toutes les tailles d’anneau. |
| Calcul vérifié | Un fait fini que le noyau a évalué, comme un contre-exemple ou une orbite périodique. | Le contre-exemple 001 → 111 de la règle 30 ; le planeur de période 16. |
| Soutenu par simulation | Aucun contre-exemple trouvé dans une recherche déclarée. C’est une conjecture, gardée comme brique ouverte. | Une régularité vue sur toutes les simulations essayées, sans preuve : elle reste une conjecture ouverte. |
| Confirmé sur le monde réel | Une prédiction enregistrée avant les données qui la tranchent, évaluée par une règle figée. C’est la seule sorte qui dise quelque chose de la nature. | Aucun pour l’instant. C’est l’étape M5 de la feuille de route. |
Une loi démontrée dans un automate cellulaire n’est pas une loi de la nature. Pour aller vers la physique, Slean rend explicite l’écart entre la première sorte et la dernière, il ne l’efface pas.