Repository navigation
fix(lean,#17357): Lean-16e -- 3 fractions de PRIMEGAME corrigees (le generateur ne produisait aucun premier) - #20129
Conversation
…gees Le carnet presente le generateur de nombres premiers de Conway, mais sa liste de fractions differait de PRIMEGAME canonique en trois positions (77/19 -> 77/29, 15/2 -> 15/14, 1/7 -> 15/2). Consequence mesuree : le programme tombait dans un 2-cycle (39875 <-> 47125) et n'affichait jamais la moindre puissance de 2 pure au-dela de la graine -- donc jamais un premier, alors que la conclusion du carnet affirme que l'etudiant l'a execute. Avec les fractions correctes, la fenetre de 20 pas affichee se termine sur 4 = 2^2 ; les exposants suivants sont les nombres premiers dans l'ordre (pas 19, 69, 280, 707, 2363 pour 2, 3, 5, 7, 11). Re-execution : 8/8 cellules, 0 erreur (4.1 s), kernel lean4-wsl. Seule la cellule de code 11 est re-executee (C.2) ; les sorties des sept autres cellules de code sont inchangees par le correctif (verifie contre un run de controle a source inchangee). See #17357 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams). Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels |
… l'executeur canonique)
Le rouge bloquant `Papermill ratchet (base vs PR)` refusait la PR : les
sorties du carnet avaient change mais le bloc `metadata.papermill` restait
byte-identique a celui d'origin/main (run du 2026-06-18). Le bloc decrivait
donc l'execution precedente, pas celle qui a produit les sorties commitees --
c'est le STALE_BLOCK que le garde detecte.
Correctif : re-execution du carnet par l'executeur canonique
(scripts/notebook_tools/wsl_papermill.py execute --kernel lean4-wsl),
papermill 2.7.0, 8/8 cellules, 0 erreur, 5.3 s. Le bloc est reecrit par
l'executeur (verdict BLOCK_MOVED, 0 regression).
Contexte d'execution : le lake naturel du carnet (conway_lean) ne rend plus
de LEAN_PATH -- le paquet Mathlib partage de .lake/packages/mathlib est sale
et lake refuse le checkout ("Please move or remove them before you switch
branches"), ce qui prive le lancement direct du REPL et fait tomber le noyau
en "FAILED DUE TO EOF". Le carnet n'importe rien (il redefinit Frac
localement) : l'execution a tourne dans un contexte lake minimal de meme
toolchain (v4.33.0) et meme binaire repl-4.33.0.
Preuves : ratchet rc=0 a la tete (1 carnet change, 0 regression) ;
prose-counts rc=0 ; les hooks pre-commit passent (H.3 inclus) ; les sorties
de 5 des 8 cellules sont byte-identiques a celles du run precedent (sequence
corrigee 1925/2275/... et 4 au pas 19 reproduites), la cellule 23 ne
differant que par le texte d'avertissement du noyau, plus detaille.
See #17357
Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Rouge
|
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[ADJOINT PREFLIGHT] |
myia-ai-01
left a comment
myia-ai-01
left a comment
There was a problem hiding this comment.
Approbation a la tete 0314d7b. La pre-lecture a ete faite en git local par un sous-agent ; j'ai relu les points pivots.
- Preuve du claim central : present: two Python simulations (carnet list vs canonical) with pure-power-of-2 sequences quoted; canonical list now yields exponents 1,2,3,5,7,11,13,17...; papermill ratchet STALE_BLOCK repaired by re-execution with block-rewriting executor (c.6087708992)
- Execution : changed code cell re-executed via canonical wsl_papermill (8/8 cells, 0 errors, 5.3s, papermill block rewritten) -- measured firsthand at head: 8/8 exec_count+outputs, 0 error outputs
- Aucune violation C.1, aucun recit d'activite ajoute.
2 participants
Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20127
Le générateur de nombres premiers ne générait aucun nombre premier — cinquième carnet de la file #17357 pour cette lane.
Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (1 constat, 0 faux positif) — et la cause réelle est plus grave que celle que l'audit décrit.
Audit source : commentaire 5844673042 (Hermes, campagne #17073 — 1 ×
stale-claimsur la cellule343763ba; l'audit conclut « proposés 1 · confirmés 1 · rejetés 0 · organes 6/6 · RAS par ailleurs »).Diff : 2 cellules, 3 champs — la liste de fractions (cellule de code 11) et sa sortie ré-exécutée, plus la cellule markdown 12.
Ce que l'audit avait vu — et c'était juste
La consigne de lecture (cellule$2, 4, 8, 16, \dots$ ) » dans la sortie affichée juste au-dessus, alors que cette sortie —
343763ba) invitait l'apprenant à « repérez les valeurs qui sont des puissances de 2 pures ([2, 15, 825, 725, 39875, 47125, 39875, 47125, …]— ne contient aucune puissance de 2 pure au-delà de la graine2(exposant 1, non premier). L'affirmation centrale de la section 5 (« une machine à 14 fractions génère les nombres premiers ») reposait donc sur une lecture que le carnet ne permettait pas de faire. Constat confirmé.Ce que l'audit n'avait pas vu — la cause, et c'est là qu'est le défaut
L'audit attribue l'absence à une fenêtre trop courte : « il faudrait ~200+ pas pour voir apparaître 4 (=2²) ». C'est faux, et mesuré faux.
La liste de fractions du carnet n'est pas PRIMEGAME. Elle en diffère en trois positions :
(77, 19)(77, 29)(15, 2)(15, 14)(1, 7)(15, 2)Le tell est visible à l'œil nu :
77/19apparaît deux fois dans la liste du carnet (positions 6 et 8).Deux simulations en Python, à partir de
N = 2:Avec les fractions du carnet, le programme boucle sur deux valeurs et ne produira jamais de premier, quel que soit le nombre de pas. L'audit a donc bien mesuré (il a simulé la liste du carnet, retrouvant les mêmes puissances de 2 pures), mais il a extrapolé la cause depuis un programme bloqué : « ~200+ pas » décrit une trajectoire qui n'arrive nulle part.
Avec PRIMEGAME,
4 = 2²apparaît au pas 19 — dans la fenêtre de 20 pas déjà affichée par le carnet. Il n'y avait rien à allonger : il y avait trois fractions à corriger.Le correctif
54ae4ad9) : les trois fractions ramenées à PRIMEGAME canonique. La sortie est ré-exécutée, pas éditée.343763ba) : la consigne dit maintenant ce que la sortie montre —La cellule d'introduction$2^2, 2^3, 2^5, 2^7, 2^{11}$ ) est laissée intacte : l'audit relève lui-même qu'elle est juste. La conclusion (cellule
0e84f3ae(qui énonce correctementd665dff2, « l'étudiant a exécuté le célèbre générateur de nombres premiers de Conway ») devient vraie par ce correctif — elle ne l'était pas avant.Ré-exécution et fidélité
Le carnet est auto-suffisant : zéro import, toutes les définitions (
Frac,fracMulNat,fractranStep,fractranRun,mkFracs) sont dans les cellules 3, 6 et 8.Contrôle de fidélité — j'ai ré-exécuté le carnet avant toute modification, pour savoir ce que l'environnement actuel reproduit tout seul :
text/plainidentique à la sortie committée0dc5173d)L'écart de la cellule 23 est un libellé de linter Lean, pas un résultat :
🟨 unused variable \prog`(committé) vs🟨 Variable name `prog` is not explicitly referenced.(re-exécuté), mêmes positions, même sévérité, même sens. Les sorties committées datent d'un run papermill du **2026-06-18** (metadata.papermill.end_time`) ; le message du linter a été reformulé depuis. Cet écart est indépendant du correctif : la cellule 23 produit exactement le même texte avant et après ma modification — je l'ai donc laissée telle quelle, pour ne pas introduire de churn sur une cellule que ma correction ne touche pas.Ce qui a été transplanté : uniquement la sortie de la cellule 11, telle que le noyau l'a produite (convertie dans la convention du fichier, listes de lignes — convention vérifiée sur les 21 sorties du carnet, 0 divergence). Aucune sortie n'a été éditée à la main.
Le tampon
metadata.papermillglobal reste celui de juin : je n'ai pas exécuté via papermill (absent de ce venv WSL) mais viajupyter_clientsur le même kernel. Le tampon est donc partiellement périmé — 7 des 8 cellules viennent bien de ce run, la cellule 11 de celui d'aujourd'hui. Je le déclare plutôt que de le réécrire.Portée du diff
Trois champs modifiés, sur 2 cellules d'un carnet de 26 — vérifié champ par champ contre
main:ids,cell_type,metadata(par cellule et global),nbformat/nbformat_minoret lesexecution_count1..8sont inchangés. Les sept autres cellules de code gardent leurs sorties d'origine.Observation hors périmètre (non traitée)
La cellule d'introduction
0e84f3aedate le programme de « 1984 (?) ». Le papier FRACTRAN de Conway est généralement daté de 1987 (Open Problems in Communication and Computation, Springer). La cellule porte déjà un point d'interrogation, donc elle ne ment pas ; je ne l'ai pas corrigée pour ne pas introduire dans cette PR une affirmation que je n'y sourcerais pas. Signalé ici.Second point, mineur : l'audit justifie la clôture par « kernel natif, cellules à exécution longue ». Mesuré, le carnet s'exécute en 4,1 s sans aucun import — il est re-exécutable par un apprenant.
See #17357— la file de cette lane compte 11 carnets ; ceci en traite 5 (Lean-11 en #20122, Lean-16a en #20123, Lean-16d en #20124, Lean-16c en #20127). Les 6 autres suivent en PR séparées ([RELEASED]à la dernière).🤖 Generated with Claude Code