Bibliothèque
Tout ce qui est accepté ou réfuté est gardé sous forme de théorèmes Lean, que les recherches suivantes réutilisent.
La mémoire de Slean
Chaque résultat accepté ou réfuté devient une brique de la bibliothèque. Une brique est un théorème Lean : on peut la vérifier à nouveau à tout moment, et la réutiliser sans la refaire.
Il y a trois sortes de briques :
- acceptée : une loi avec son certificat vérifié ;
- réfutée : une affirmation fausse avec son contre-exemple vérifié ;
- ouverte : une conjecture soutenue par la simulation, sans preuve. Elle reste marquée comme ouverte, jamais comme vraie.
La première bibliothèque
La bibliothèque actuelle contient toutes les lois de conservation de largeur au plus 3 des 256 automates élémentaires, hors lois triviales : 84 lois sur 66 règles. Chacune est démontrée pour des anneaux de toutes les tailles. La commande lake build les vérifie toutes à nouveau en une vingtaine de secondes.
Vous pouvez les parcourir ci-dessous. Le navigateur recalcule l’automate à partir de son numéro de règle et additionne la densité de la loi choisie sur chaque ligne.
Une loi de la bibliothèque, recalculée dans votre navigateur
La règle 184 est un modèle de trafic : une voiture, case noire, avance d’une case si la case devant elle est libre. Chaque ligne est un pas de temps, de haut en bas, sur un anneau de 64 cases. La bibliothèque contient une loi pour cette règle : le nombre de cases libres ne change jamais, donc celui des voitures non plus.
Total de la densité : 36 à chacun des 40 pas.
- 0
- 1
- 1
- 0
Poids de chaque motif lu à partir d’une case, tels qu’ils figurent dans la brique b00047 de la bibliothèque. Les nombres à droite de la figure sont le total de ces poids sur la ligne.
Cette figure est une simulation : elle montre la loi sur une configuration et 40 pas. La preuve, elle, vaut pour toutes les tailles et toutes les configurations. C’est le théorème conserved_of_fluxCheck appliqué au certificat de flux que le noyau a vérifié.
La figure est une simulation sur une configuration et 40 pas. La preuve, elle, vaut pour toutes les tailles et toutes les configurations : c’est le théorème conserved_of_fluxCheck appliqué au certificat que le noyau a vérifié.
Réutiliser
La bibliothèque sert à ne pas refaire ce qui est fait. Un explorateur peut partir des lois déjà connues d’un monde voisin. La mesure vérifie si cela aide vraiment : c’est la comparaison entre un passage à froid et un passage avec bibliothèque, décrite dans Mesurer une découverte. Sur les lois de conservation, la mémoire n’a presque rien fait gagner, parce que la méthode à froid est déjà presque optimale.