Inspirations

Slean n’est pas né de rien. Voici ce que nous empruntons à chaque source, et ce que nous ne prétendons pas.

Lean et Mathlib

Lean est un langage de programmation et un assistant de preuve : un petit noyau de Leannoyau de Lean Lean est un logiciel qui vérifie des preuves mathématiques. Son noyau est un petit programme qui contrôle chaque étape. S’il accepte, la preuve est correcte, sans avoir à croire quiconque sur parole. y vérifie chaque preuve. Mathlib est sa bibliothèque mathématique partagée.

• Ce que nous empruntons : des preuves vérifiées par le noyau, une bibliothèque commune qui s’accumule, et une frontière explicite des énoncés encore ouverts. Slean, c’est Science + Lean.
• Ce que nous ne prétendons pas : Slean n’est pas un nouveau langage formel, et une loi démontrée dans un monde simulé n’est pas un théorème sur la nature.

Physlib

Physlib formalise de la physique en Lean.

• Ce que nous empruntons : ses définitions, que Slean réutilisera pour les mondes de la physique (étape M4 de la feuille de route) plutôt que de les dupliquer.
• Ce que nous ne prétendons pas : Slean ne remplace pas Physlib et ne l’a pas encore utilisé.

Wolfram Physics Project

Le Wolfram Physics Project explore l’espace des règles simples et y cherche des structures émergentes.

• Ce que nous empruntons : la méthode : énumérer des règles, simuler, chercher des régularités.
• Ce que nous ne prétendons pas : nous ne reprenons pas ses conclusions, qui n’ont pas encore de prédiction testable acceptée.

Minimo

« Learning Formal Mathematics From Intrinsic Motivation », Poesia, Broman, Haber et Goodman, NeurIPS 2024 (arXiv 2407.00695) : un agentagent Un programme d’IA qui travaille seul : il lance des expériences, propose des affirmations et lit les réponses du vérificateur. qui pose ses propres conjectures et les démontre à partir des seuls axiomes.

• Ce que nous empruntons : l’idée d’une exploration ouverte, sans cible fixée à l’avance.
• Ce que nous ne prétendons pas : Slean ne fait pas encore de découverte ouverte ; ses agents répondent à des types d’affirmation imposés.

STP

« Self-play LLM Theorem Provers with Iterative Conjecturing and Proving », Dong et Ma, ICML 2025 (article) : un conjectureur et un prouveur qui s’entraînent l’un l’autre en Lean.

• Ce que nous empruntons : le couple proposer, vérifier, où le vérificateur exact donne le signal.
• Ce que nous ne prétendons pas : Slean n’entraîne pas de modèle aujourd’hui.

Dream-RSI

« Recursive Self-Improvement through Evolving Worlds », Zheng et al., 2026 (arXiv 2609.14858) : rejouer des arbres de découverte enregistrés pour améliorer la politique d’exploration à moindre coût.

• Ce que nous empruntons : l’idée de garder chaque exploration pour la rejouer. Cela exige des scores déterministes, et c’est ce que fournit le vérificateur exact de Slean.
• Ce que nous ne prétendons pas : Slean n’a pas encore mis en place cette boucle d’amélioration.

La boucle autoresearch de Karpathy

La boucle autoresearch d’Andrej Karpathy, proposer, lancer, garder ou jeter, est l’ancêtre du moteur de Mutome. Slean fournit l’étape « garder ou jeter » avec un juge exact plutôt qu’une impression.

Pour la suite, voir Slean en 5 minutes et Quatre sortes de preuves.