Quatre sortes de preuves

Démontré dans un monde, calcul vérifié, soutenu par simulation, confirmé sur le monde réel : quatre choses différentes, jamais fondues en une note.

Pourquoi les séparer

« C’est prouvé » peut vouloir dire des choses très différentes. Slean garde quatre sortes de preuves séparées, et chaque résultat dit de quelle sorte il est.

Quatre sortes de preuves

Sorte	Ce que cela veut dire	Exemple dans Slean
Démontré dans un monde	Un théorème Lean sur la définition exacte d’un monde. Vrai pour ce monde, sans condition.	Le trafic : le nombre de voitures est conservé pour toutes les tailles d’anneau.
Calcul vérifié	Un fait fini que le noyau a évalué, comme un contre-exemple ou une orbite périodique.	Le contre-exemple 001 → 111 de la règle 30 ; le planeur de période 16.
Soutenu par simulation	Aucun contre-exemple trouvé dans une recherche déclarée. C’est une conjecture, gardée comme brique ouverte.	Une régularité vue sur toutes les simulations essayées, sans preuve : elle reste une conjecture ouverte.
Confirmé sur le monde réel	Une prédiction enregistrée avant les données qui la tranchent, évaluée par une règle figée. C’est la seule sorte qui dise quelque chose de la nature.	Aucun pour l’instant. C’est l’étape M5 de la feuille de route.

Sorte

Ce que cela veut dire

Exemple dans Slean

Démontré dans un monde

Un théorème Lean sur la définition exacte d’un monde. Vrai pour ce monde, sans condition.

Le trafic : le nombre de voitures est conservé pour toutes les tailles d’anneau.

Calcul vérifié

Un fait fini que le noyau a évalué, comme un contre-exemple ou une orbite périodique.

Le contre-exemple 001 → 111 de la règle 30 ; le planeur de période 16.

Soutenu par simulation

Aucun contre-exemple trouvé dans une recherche déclarée. C’est une conjecture, gardée comme brique ouverte.

Une régularité vue sur toutes les simulations essayées, sans preuve : elle reste une conjecture ouverte.

Confirmé sur le monde réel

Une prédiction enregistrée avant les données qui la tranchent, évaluée par une règle figée. C’est la seule sorte qui dise quelque chose de la nature.

Aucun pour l’instant. C’est l’étape M5 de la feuille de route.

Slean ne les mélange jamais en une seule note.

Lire le tableau

Démontré dans un monde : la loi du trafic est vraie pour toutes les tailles d’anneau de la règle 184. C’est un théorème sur une définition exacte, rien de plus.
Calcul vérifié : le contre-exemple de la règle 30, ou un planeur qui revient après 16 pas. Un fait fini, que le noyau a évalué.
Soutenu par simulation : aucune exception trouvée dans une recherche déclarée. C’est une conjecture, gardée comme brique ouverte.
Confirmé sur le monde réel : une prédiction enregistrée avant que les données qui la tranchent n’existent, évaluée par une règle fixée à l’avance. C’est la seule sorte qui dise quelque chose de la nature.

Ce que Slean ne prétend pas

Une loi démontrée dans un automate cellulaire n’est pas une loi de la nature. Aujourd’hui, Slean produit les deux premières sortes, et parfois la troisième. La quatrième viendra avec l’étape M5 de la feuille de route. Pour aller vers la physique, Slean rend explicite l’écart entre la première sorte et la dernière, il ne l’efface pas.