Feuille de route
Chaque étape se termine par une mesure. Quand un explorateur ne bat pas les méthodes génériques, c’est la conception qui change. On n’ajoute pas d’interface, de périmètre ou de vocabulaire pour compenser.
M1 · Fondation Fait
- Les automates cellulaires comme mondes Lean, et le théorème de flux : un certificat local démontre la conservation pour toutes les tailles.
- Une bibliothèque vérifiée par le noyau : les 84 lois de conservation de largeur au plus 3 des automates élémentaires.
- Un moteur avec vérificateur, bibliothèque, explorateurs, et un protocole qui compare le passage à froid et le passage avec mémoire.
- Constat : les lois de conservation additives en dimension 1 sont résolues par l’ajustement exact, 20 lois sur 20 en 24 propositions. Cette classe calibre la machinerie, elle ne démontre pas la découverte.
M2 · Des découvertes sans recette En cours
- Fait : des laboratoires mesurés. Tout agent passe par ./lab ; mises à jour de cellules, propositions, jetons et coût sont comptés, les réponses cachées restent dehors, les transcriptions sont auditées, les résultats sont exportés en Lean.
- Fait : les structures localisées comme deuxième type de découverte, avec témoins et réfutations vérifiés par le noyau.
- Fait : un scientifique de référence scripté qui utilise exactement l’interface et le budget de l’agent.
- Fait : des mondes compressibles (règles de 1 024 entrées cachant une loi courte) où inférer la loi est la tâche. Les leçons gagnent 8 paires répétées sur 9 (+6 par labo) et aident à trouver des lois compactes, mais font seulement jeu égal avec une référence scriptée par induction.
- Des mondes qu’une seule expérience ne suffit pas à identifier : observation partielle, bruit, grands espaces d’états.
- Réversibilité : un certificat de règle inverse quand la règle est réversible, une collision quand elle ne l’est pas.
- Isomorphismes comme briques : « le monde B est le monde A renommé », avec un théorème de transport, pour qu’une relation découverte redémontre toutes les lois de A dans B. C’est la première vraie dépendance entre briques.
- Des types d’affirmation ouverts : l’agent définit ses propres propriétés décidables en Lean, et leur intérêt est jugé par l’usage qui en est fait ensuite.
- Des explorateurs mesurés sur plusieurs graines face à l’ajustement exact et à la force brute, à coût compté égal.
M3 · Mutome tourne sur Slean À venir
- Les labos Slean deviennent un type de campagne autoresearch de Mutome : Mutome mesure son « Harness Lift » sur des mondes dont les réponses sont cachées.
- La bibliothèque devient la mémoire vérifiée de Mutome : ce qu’une campagne a établi, la suivante le réutilise sans le revérifier à la main.
- Le fonctionnement continu de Mutome appelle le moteur et écrit dans une bibliothèque qui grandit.
- mutome.com montre la bibliothèque vivante : briques, réfutations, conjectures ouvertes et graphe de dépendances.
M4 · Mondes de la physique À venir
- Systèmes sur réseau et systèmes hamiltoniens définis en Lean, en réutilisant les définitions de Physlib quand elles existent.
- Quantités exactement conservées par des intégrateurs discrets, symétries, énoncés de stabilité.
- La boucle : simuler, conjecturer, démontrer, ou réfuter par un contre-exemple vérifié.
M5 · Le monde réel À venir
- Données d’ingénierie, de biologie et de physique, avec une vérification prospective : Mutome enregistre une prédiction et sa règle d’évaluation avant que les données décisives n’existent, et Slean l’évalue avec un évaluateur figé.
- Les bancs d’essai rétrospectifs ne sont admis qu’avec des partitions figées et sans notation répétée sur les mêmes données réservées.
Ce que Slean ne cherche pas à être
- Un nouveau langage formel. Le langage, c’est Lean.
- Un standard de métadonnées ou de provenance. La provenance est enregistrée, mais ce n’est pas le produit.
- Un service hébergé ou une interface publique avant d’avoir la preuve que le moteur découvre.
- Une copie de Physlib, de Mathlib ou des codes de simulation existants. Slean les réutilise.