Skip to content

fix(lean,#17357): Lean-16d -- deux affirmations fausses (axiomes, exercice 3) #20124

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 1 commit into from
Oct 10, 2026
Merged

fix(lean,#17357): Lean-16d -- deux affirmations fausses (axiomes, exercice 3) #20124

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-16d-Conway-Game-of-Life-Lean-Native.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1190,7 +1190,7 @@
"\n",
"## 9. La frontière du prouvé : transparence\n",
"\n",
"Les théorèmes ci-dessus ne dépendent **d'aucun axiome caché** — en particulier pas de `sorry`. Vérifions-le :\n",
"Trois de ces théorèmes ont été fermés par `decide`, le quatrième par `native_decide` : `#print axioms` va montrer que les deux tactiques ne laissent pas la même trace. Vérifions :\n",
"\n",
"**Pourquoi cela compte-t-il ?** En Lean, une tactique comme `decide` ou `native_decide` ferme un but en *évaluant* un terme, mais la confiance que l'on accorde au résultat repose sur ce que le noyau accepte. La commande `#print axioms` est l'**ancre de confiance** : elle liste tous les axiomes dont un théorème dépend transitivement. Si elle renvoie une liste vide, le théorème est **auto-contenu** — prouvé à partir des seules règles du calcul des constructions. Une preuve qui admettrait un axiome ad hoc (ou un `sorry` masqué) apparaîtrait ici. C'est précisément ce qui distingue une **formalisation** (le noyau certifie, tous les cas couverts) d'un **test** (on a vérifié un échantillon d'entrées) : le test peut rater un contre-exemple, la formalization ne le peut pas.\n"
]
Expand Down Expand Up @@ -1621,7 +1621,7 @@
"\n",
"### Exercice 3 — Un nouvel oscillateur\n",
"\n",
"Définissez le **pulsar** miniature ci-dessous et vérifiez qu'il est de période 2 (set-égalité avec `sameSet`). *Indice : inspirez-vous des définitions de `blinker`/`toad`.*\n"
"Définissez un **oscillateur de période 2** ci-dessous et vérifiez-le (set-égalité avec `sameSet`). *Indice : inspirez-vous des définitions de `blinker`/`toad`.*\n"
]
},
{
Expand Down
Loading