Skip to content

feat(geometry,#18608): notebook Geometry-04 — DD+AR, la moitie symbolique d'AlphaGeometry - #18610

Merged
myia-ai-01 merged 4 commits into
mainfrom
feature/geometry-04-ddar
Oct 1, 2026
Merged

myia-ai-01 merged 4 commits into
mainfrom
feature/geometry-04-ddar

Conversation

@jsboige

@jsboige jsboige commented Sep 30, 2026

Copy link
Copy Markdown
Owner

Grain: DEEP/notebook-python — lane myia-po-2023:CoursIA — prev: MED/refactor #18607

Position 04 du programme gradué #17544, issue de qualification #18608. Stack : basée sur feature/geometry-reparenting (PR #18607) — à retargeter sur main après son merge ; le diff ci-contre ne contient que le 04. See #18608.

Ce que le notebook établit

Geometry-04-DD-AR-Python.ipynb (25 cellules : 14 md + 11 code) construit la moitié symbolique d'AlphaGeometry :

  • DD : faits géométriques sous forme canonique (symétries neutralisées), corpus de 5 règles élémentaires, fermeture à point fixe, trace de preuve remontable par fait dérivé (proof_chain).
  • Le fil rouge, 4e regard : triangle rectangle en A, M milieu de [BC] — la fermeture dérive BM = CM et l'alignement, et s'arrête devant MA = MB : la limite combinatoire d'AlphaGeometry sans point auxiliaire devient un enseignement (§2), pas un défaut.
  • AR : la traduction polynomiale de 01/02 réutilisée — MA²−MB² et MA²−MC² réduits à zéro par sympy.groebner des hypothèses (§3).
  • Témoin négatif : MA² = MB²/16 rejeté deux fois — jamais dérivé par DD, résidu 15(xc²+yc²)/64 non nul sauf figure dégénérée C=B (§4).
  • 3 exercices C.1 (règle coll_trans à ajouter, chaîne de preuve à lire, énoncé faux à réfuter) — stubs print("Exercice a completer"), aucune erreur volontaire.

Les 5 questions organ-first (qualification #18608)

  1. Quelle série possède déjà la sémantique ? Mesuré le 30/09 (Geometry 04 — Raisonner comme un geometer (DD+AR) : qualification d'organe (issue fille de #17544) #18608) : SemanticWeb/SW-13 (owlrl/OWLReady2, monde ouvert), SW-6b (RDFS, trop faible), SW-16 (preuve embarquée — complément pour la trace). Pour AR : sympy (organe de 01/02/03).
  2. Peut-on invoquer leur module réel ? Pour AR oui et fait : sympy.groebner est appelé tel quel (cellule §3), aucune réimplémentation. Pour DD : aucun moteur DD fermé sur prédicats n-aire géométriques n'existe dans le dépôt (grep mesuré, Geometry 04 — Raisonner comme un geometer (DD+AR) : qualification d'organe (issue fille de #17544) #18608).
  3. Faut-il exporter/refactorer la série source ? Non — l'écart n'est pas une extraction : la sémantique DD géométrique n'existe nulle part.
  4. Témoin négatif de l'organe natif ? sympy.groebner fournit le témoin du §4 (résidu non nul) — l'organe natif rejette l'énoncé faux.
  5. Quelle autre série vérifie indépendamment ? 02 (Gröbner) et 03 (Wu) ont prouvé le même fil rouge par d'autres voies — le tableau §5 du notebook croise les quatre regards.

Copie pédagogique déclarée (motif : le moteur DD à ~100 lignes EST le didacticiel, comme la pseudo-division from scratch du 03 contre-vérifiée par sympy.prem) — déclarée en §1 du notebook et ici.

Verdict SOTA

SOTA-OK pour AR (sympy réel, sorties committées = ses vraies sorties). Le moteur DD relève de la copie pédagogique déclarée ci-dessus — pas d'outil équivalent installable : les reasoners OWL mesurés (#18608) sont open-world, inadaptés au DD fermé n-aire.

Validation

  • Papermill in-place kernel python3 : 25/25 cellules, 2.4 s (exigence < 1 min ✓), execution_count != null + outputs sur les 11 cellules code (H.3 pre-commit Passed).
  • 0 erreur, 0 raise NotImplementedError (grep pre-commit Passed).
  • check_notebook_nav_chain.py --check --diff-files : rc=0 (04 reachable, aucun finding nouveau — baseline inchangée, aucun orphan_entry pour 04).
  • Pre-commit 12/12 Passed (gitleaks, probeAddresses, papermill paths, H.3, source-parses).
  • READMEs (série + famille) : position 04 « Livré », parcours léger, coûts — totaux laissés au catalogue (byte-identique, règles catalog-pr-hygiene).

🤖 Generated with Claude Code

jsboige and others added 2 commits September 30, 2026 18:06
…licAI/Lean/Geometry/ (tranche 1)

git mv 4 notebooks + README sous Lean/, reecriture des referents (README famille,
curriculum, regen_quarto_render, baseline nav-chain), sans changement de contenu.
Catalogue byte-identique (regen par l'automatisation). See #18601 (tranche 1/volet A).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
…lique d'AlphaGeometry

Moteur DD (fermeture a point fixe, trace de preuve remontable, corpus de 5
regles elementaires) + AR (sympy.groebner, l'organe de 01/02 reutilise).
Fil rouge : 4e regard -- DD derive MB=CM et s'arrete devant MA=MB (limite
combinatoire sans construction), AR prouve les deux cibles par reduction
a zero. Temoin negatif : MA^2=MB^2/16 rejetee deux fois (jamais derive +
residu 15(xc^2+yc^2)/64 non nul sauf figure degeneree). 3 exercices C.1,
execution Papermill 2.4 s, 0 erreur, sorties commitees. Copie pedagogique
declaree : le moteur DD est le didacticiel (qualification #18608).
READMEs serie + famille mis a jour (04 Livre, parcours leger). See #18608.

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions

Copy link
Copy Markdown
Contributor

Base != main (advisory, #10918)

Cette PR ne livre pas sur main : son contenu attend le merge de feature/geometry-reparenting. 1 PR ouverte(s) de feature/geometry-reparenting vers main existe(nt) a cet instant -- c'est un stack legitime, le contenu est en vol. Verifier au moment du merge que la base est effectivement reliee a main.

Couverture CI perdue sur cette base (mesure, #16194)

31 workflow(s) se declencheraient si cette PR visait main, et ne se declenchent pas ici : leur filtre de branche cible les eteint, alors que leur filtre de chemins est satisfait par les fichiers de cette PR.

  • always-on-guards.yml
  • banner-guard.yml
  • bare-cross-dir-load-gate.yml
  • catalog-drift.yml
  • cell-order-gate.yml
  • consecutive-code-cells-advisory.yml
  • enrich-quality-gate.yml
  • markdown-claims-output-advisory.yml
  • markdown-rendering-guard.yml
  • mermaid-fill-color-advisory.yml
  • notebook-cell-source-parses.yml
  • notebook-exec-sequence-ratchet.yml
  • ... et 19 autre(s)

Un check absent n'est pas un check vert. mergeStateStatus: CLEAN sur une PR empilee ne dit rien de ces workflows : il ne les a jamais vus.

@github-actions

github-actions Bot commented Sep 30, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #18610 (feat(geometry,#18608): notebook Geometry-04 — DD+AR, la moitie symbolique d'AlphaGeometry) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

# Conflicts:
#	MyIA.AI.Notebooks/SymbolicAI/README.md
@github-actions

Copy link
Copy Markdown
Contributor

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

…4 (leve orphan_entry check-nav-chain)

Le retarget de #18610 sur main (base #18607 squash-mergee) laissait un
conflit reel sur SymbolicAI/README.md et un rouge check-nav-chain :
Geometry-04 etait une entree orpheline (aucune arete de navigation
entrante, la serie n'en portait aucune). Resolution :

- README SymbolicAI : conflit resolu cote branche (ligne 04 livree,
  'A venir' mis a jour) ;
- Geometry-03b : ligne de navigation a sens unique vers Geometry-04
  (convention fleche, cf docstring de check_notebook_nav_chain) +
  reference croisee dans 'Dans ce depot'. Markdown-only, pas de
  re-exec due (C.2 exception), pas de paire twin (verifie).

check_notebook_nav_chain --check --diff-files : 0 NEW finding.
Les 2 findings Lean-15b/15c resolus par le merge de main ne sont pas
touches (baseline = sujet separe).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions github-actions Bot added the pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) label Sep 30, 2026
@github-actions

Copy link
Copy Markdown
Contributor

PR gate absent du rollup (advisory, #10928)

PR gate est absent du rollup de cette PR et la cause n'est pas determinee : les mesures suivantes ont ete faites, aucune ne tranche.

  • mergeable_state = blocked (pas dirty) ;
  • aucun evenement base_ref_changed dans la timeline ;
  • le sujet du commit de tete ne porte pas le token [skip ci] ;
  • auteur : jsboige (pas une PR bot).

Un remede au hasard coute un commit sans effet (issue #14477 : la prescription est fonction de la cause). Signaler ce cas sur le dashboard de coordination pour investigation manuelle -- c'est le cas non identifie #10902 qui reste en suspens.

Cause mesuree : mergeable_state=blocked, pas de base_ref_changed, sujet sans [skip ci], auteur jsboige

@github-actions

Copy link
Copy Markdown
Contributor

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

@github-actions

Copy link
Copy Markdown
Contributor

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

@github-actions

Copy link
Copy Markdown
Contributor

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

@github-actions

Copy link
Copy Markdown
Contributor

✅ 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 factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

@github-actions github-actions Bot added the consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) label Sep 30, 2026
@github-actions

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 3.2s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 3.3s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 3.9s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 4.1s
Search-01-StateSpace.ipynb ✅ SUCCESS 3.1s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 1.9s
rl_4_multi_armed_bandits.ipynb ✅ SUCCESS 14.2s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 2.4s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

@github-actions

Copy link
Copy Markdown
Contributor

Notebook PR Validation: PASS

  • Notebooks checked: 2
  • Code cells validated: 26
  • Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

@jsboige

jsboige commented Oct 1, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-ai-01:CoursIA-2
pr: 18610
head: 2d39171
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: ef9304ecc18d04fcdd26fb9f839f70dacd1076be7974297477af15b6545f1375
diff-files: 4
diff-additions: 945
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

@github-actions github-actions Bot added the large-pr-no-review PR > seuil sans review (ni bot ni humaine) -- retire quand une review arrive (#11232) label Oct 1, 2026
@github-actions

github-actions Bot commented Oct 1, 2026

Copy link
Copy Markdown
Contributor

Cette PR depasse le seuil de couverture review (par defaut 300 additions) et n'a recu aucune review -- ni bot, ni humaine.

Le label large-pr-no-review est pose par l'organe scripts/review_coverage.py porte par l'issue #11232. Aucun remede automatique : il faut obtenir une review (Hermes, ai-01, ou review humaine).

Le label est retire au balayage suivant (quotidien) des qu'une review arrive -- dans reviews[] ou en commentaire de verdict -- ou que le diff passe sous le seuil. Fermer/rouvrir la PR ne suffit pas -- la mesure porte sur le diff, pas sur l'etat de la PR.

Seuil, historique et exceptions : cf. docs/reference/review-coverage-threshold.md.

@myia-ai-01
myia-ai-01 merged commit f45b22e into main Oct 1, 2026
94 of 96 checks passed
jsboige added a commit that referenced this pull request Oct 2, 2026
Resolution: theirs (main) pour les 5 fichiers en conflit (HEAD
n'apporte pas de substance sur ces fichiers ; main est plus recent
sur chacun -- cf. done_c43_pending.md) :
  * MyIA.AI.Notebooks/GenAI/RAG-et-Memoire-Semantique/06-KernelMemory-InProcess.ipynb (#18627 > #18619)
  * MyIA.AI.Notebooks/Probas/README.md (#18613 > #18426)
  * MyIA.AI.Notebooks/SymbolicAI/Argument_Analysis/Argumentation-02-Fallacies-Detection-Python.ipynb (#18781 > #18506)
  * MyIA.AI.Notebooks/SymbolicAI/README.md (#18610 > #18607)
  * _quarto.yml (#18710 > #18616)

Auto-merge reussi sur les autres fichiers modifies par main
(notebooks case studies, complexite, workflows, etc.).

Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) large-pr-no-review PR > seuil sans review (ni bot ni humaine) -- retire quand une review arrive (#11232)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants