Questions fréquentes

Est-ce de la vraie science ?

Pas encore, et nous ne le prétendons pas. Slean démontre des lois dans des mondes exacts, et mesure si un agent les trouve. Une loi démontrée dans un automate cellulaire n’est pas une loi de la nature. Le but est de construire, sur des mondes où la vérité est connue, les outils qui permettront ensuite de juger des découvertes sur des systèmes plus riches. Voir Quatre sortes de preuves.

Pourquoi des automates cellulaires ?

Parce qu’ils sont exacts, rapides à simuler, et qu’on peut en générer autant qu’on veut. Pour chaque monde généré, la réponse complète peut être calculée à l’avance, ce qui permet une note honnête. Leurs lois, quantités conservées et structures qui se déplacent, ont des analogues en physique. Ce sont des mondes de calibration : les mondes de la physique viendront à l’étape M4.

Pourquoi Lean si Python vérifie déjà ?

Pour un fait fini, comme un contre-exemple ou un planeur qui revient après 16 pas, le calcul de Python est déjà exact. Le noyau de Lean ajoute une garantie indépendante : un deuxième vérificateur, petit et très éprouvé, qui ne partage pas les bugs du moteur. Lean devient indispensable pour les énoncés universels, comme « pour toutes les tailles d’anneau » : aucune simulation ne peut les couvrir, seule une preuve le peut.

Quel rapport avec Mutome ?

Mutome est un laboratoire de recherche autonome. Mutome apporte le hasard dans la découverte, Slean le déterminisme dans la vérification. Mutome décide quoi explorer ; Slean dit ce qui est vrai, le garde, et mesure si l’exploration a aidé. À l’étape M3, les labos Slean deviennent un type de campagne d’autorecherche, pour que Mutome mesure son « Harness Lift », ce que son harnais apporte, sur des mondes à réponse cachée, et la bibliothèque devient la mémoire vérifiée de Mutome.

Qu’est-ce qui ne marche pas encore ?

• Les mondes actuels s’identifient en une seule expérience. Ce n’est pas encore de la découverte ouverte. Voir Un monde caché reconstruit.
• Un seul type de monde et deux types de découverte.
• Deux graines, un passage chacune, un seul modèle d’agent.
• La mémoire n’a pas encore montré de gain : sur les lois de conservation, il n’y avait presque rien à économiser.
• Les types d’affirmation sont fixés à l’avance ; l’agent ne choisit pas encore ses propres questions.
• Rien n’est encore confirmé sur le monde réel.

Le code est-il ouvert ?

Pas pour l’instant. Le dépôt de Slean est privé. L’accès est donné sur demande.