Glossaire

Monde

Un système exact dont les règles sont définies en Lean. Aujourd’hui, un automate cellulaire à une dimension sur un anneau. Voir Monde.

Règle

La table qui donne le nouvel état d’une case à partir de son voisinage. Pour les 256 automates élémentaires, elle est résumée par un numéro, comme 184 ou 30.

État quiescent

Un état q tel qu’un voisinage entièrement fait de q redonne q. C’est un fond calme : rien n’y naît de nulle part. Les structures localisées sont posées sur un tel fond.

Densité

Une façon de compter : un poids pour chaque case, ou pour chaque fenêtre de quelques cases, additionné sur tout l’anneau. Une loi de conservation dit que ce total ne change jamais.

Courant (flux)

Un nombre sur chaque frontière entre deux cases, qui dit ce qui la traverse pendant un pas. Si la variation de chaque case égale ce qui entre moins ce qui sort, le total est conservé.

Certificat

L’objet fini qui accompagne une affirmation et que le noyau vérifie. Pour une loi de conservation, c’est le courant. Voir Affirmation et certificat.

Réfutation

Le rejet d’une affirmation fausse, avec un contre-exemple vérifié par le noyau. Voir Réfutation.

Témoin

La configuration concrète qui sert de preuve finie : le contre-exemple d’une réfutation, ou le bloc d’une structure qui revient.

Brique

Un résultat gardé dans la bibliothèque sous forme de théorème Lean : accepté, réfuté, ou ouvert quand il n’est que soutenu par simulation.

Bibliothèque

L’ensemble des briques. C’est la mémoire que les recherches suivantes réutilisent. Voir Bibliothèque.

Labo

Le dossier où travaille un agent, avec une description de la tâche et la commande ./lab. Voir Labo.

Budget

Les plafonds d’un passage : nombre de propositions et nombre de mises à jour de cellules.

Réponse cachée

La liste complète de ce qu’il y a à trouver dans un monde noté, calculée à l’avance et gardée hors du labo.

Référence scriptée

Un scientifique automatique, sans modèle de langage, qui utilise les mêmes commandes et le même budget que l’agent. C’est la barre à franchir.

Froid et chaud

Un passage à froid part de rien. Un passage à chaud part de la bibliothèque construite sur d’autres mondes. La différence mesure ce que la mémoire apporte.

Hors bornes

Une structure vérifiée qui dépasse les bornes de la réponse cachée, par exemple une période de 16 quand la réponse s’arrête à 8. Voir Un planeur.

Noyau Lean

Le petit programme au cœur de Lean qui vérifie chaque preuve. Dans Slean, il décide ce qui est vrai, jamais l’explorateur.