Geometry 04 — Raisonner comme un geometer (DD+AR) : qualification d'organe (issue fille de #17544)

[jsboige]

Position 04 du programme gradué #17544 — qualification d'organe avant écriture

Issue fille exigée par #17544 (« 04 et 05 viennent après la première volée. Chacun passe par une issue fille qui qualifie son organe avant d'écrire »). La première volée (01 #17581, 02 #17588, 03 #17511) et l'accrétion 03b sont mergées ; le re-parenting vers SymbolicAI/Lean/Geometry/ est en cours (#18601 tranche 1 = PR #18607).

Ce que doit faire le notebook 04

« Raisonner comme un géomètre » : base de déduction à règles (DD) et raisonnement algébrique (AR) — la moitié symbolique de la famille AlphaGeometry, sans réseau. Public : Licence. Suppose : 01 et 03. Le théorème fil rouge (milieu de l'hypoténuse équidistant des trois sommets) est prouvé une troisième fois, par exploration de règles ; le corpus de règles géométriques (points, collinéarités, milieux, distances, cercles…) est forward-chained jusqu'à fermeture, AR (sympy) servant d'oracle algébrique aux prédicats quantitatifs.

Investigation d'organe (menée le 30/09, lecture seule, à reprendre par la lane implémentante)

Organe candidat	Mesure firsthand	Fit pour DD géométrique
SemanticWeb/SW-13-Python-Reasoners.ipynb	reasoners OWL (owlrl, OWLReady2, reasonable) sur graphe RDF — hypothèse du monde ouvert, inférence de classes	Faible : DD est fermé (close-world) sur prédicats géométriques fixes ; OWL-RL y serait un carcan (non-unicité des noms, monde ouvert à désactiver)
SemanticWeb/SW-6b-Python-RDFS.ipynb	forward chaining RDFS (subsomption)	Trop faible : aucune règle n-aire (un milieu relie 3 points)
SemanticWeb/SW-16-Python-ProofCarryingOntologies.ipynb	preuve embarquée, traçabilité	Pertinent en complément : la trace de preuve DD (chaîne de règles) est un livrable pédagogique du 04
sympy	déjà l'organe AR de la série (02 Gröbner, 03 pseudo-division)	Oui pour AR — pas de réimplémentation
Moteur de règles dédié ~200 lignes (style ddar d'AlphaGeometry)	à écrire	Recommandé comme « copie pédagogique déclarée » : le moteur EST le didacticiel, comme la pseudo-division from scratch du 03 (contre-vérifiée par sympy.prem)

La PR du 04 répondra nominativement aux 5 questions organ-first (organ-first-implementation.md) — l'investigation ci-dessus les pré-remplit, la lane la confirme ou la réfute avec preuves.

Règles de fabrication (reprises de #17544, non renégociables)

1. Suppose uniquement 01 et 03 ; s'ouvre sur « Ce que ce notebook suppose » + étiquette de public (Licence).
2. Aucun résultat de recherche sur le chemin principal — IMO-AG-30 et le proposeur neuronal restent en 04b.
3. Fil rouge : le milieu de l'hypoténuse prouvé par DD+AR, troisième regard sur le même objet (01 numérique, 02 Gröbner, 03 Wu, 04 DD+AR).
4. Un témoin négatif : un énoncé faux que la fermeture DD ne prouve pas (et pourquoi).
5. Trois exercices, stubs non bloquants (C.1), exécution de bout en bout avec sorties (C.2), CPU < 1 min.
6. Organ-first : les 5 questions dans le body de la PR ; la copie pédagogique (moteur DD) se déclare avec son motif.
7. README de série mis à jour (position 04 « Livré ») + ligne du parcours léger.

Acceptance

• Notebook Geometry-04-DD-AR-Python.ipynb dans SymbolicAI/Lean/Geometry/ (post-re-parenting), exécution Papermill SUCCESS, < 1 min
• Fil rouge prouvé par DD+AR, avec trace de preuve lisible (chaîne de règles montrée)
• Témoin négatif présent et commenté
• 3 exercices C.1, aucune erreur volontaire
• Body PR : 5 questions organ-first répondues + verdict SOTA écrit
• README série + SymbolicAI/README.md (parcours léger) mis à jour — totaux laissés au catalogue
• Baseline nav-chain mise à jour si nouveaux findings (chirurgicalement, jamais snapshot complet)

See #17544 (programme) · See #18601 (re-parenting) · Référence : Trinh et al., Solving olympiad geometry without human demonstrations, Nature 2024 (DD+AR = moitié symbolique).

[jsboige]

[CLAIMED] lane myia-po-2023:CoursIA — notebook Geometry-04-DD-AR-Python + moteur DD pedagogique (copie pedagogique declaree, qualification #18608) — paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/Geometry-04-DD-AR-Python.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/README.md, MyIA.AI.Notebooks/SymbolicAI/README.md, scripts/tests/baseline_nb_nav_chain.json (branche stack sur feature/geometry-reparenting en attendant le merge de #18607)

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

[jsboige]

[INFO] lane myia-po-2023:CoursIA — notebook Geometry-04 livre : PR #18610 (stack sur feature/geometry-reparenting, a retargeter sur main apres merge de #18607). DD (fermeture + trace de preuve, 5 regles) + AR (sympy.groebner) ; fil rouge 4e regard, temoin negatif rejetee deux fois, 3 exercices C.1, Papermill 25/25 en 2.4 s, nav-chain --check rc=0. Copie pedagogique declaree + verdict SOTA-OK dans le body.

[jsboige]

[INFO] candidate-delivered — PR #18610 livre la qualification Raisonner comme un geometer (DD+AR) pour Geometry 04 #18608.

Mesure first-hand :

• PR feat(geometry,#18608): notebook Geometry-04 — DD+AR, la moitie symbolique d'AlphaGeometry #18610 MERGED 2026-10-01T15:12:41Z
• Issue Geometry 04 — Raisonner comme un geometer (DD+AR) : qualification d'organe (issue fille de #17544) #18608 (Geometry 04 — Raisonner comme un geometer, qualification DD+AR) — acceptation par le merge de feat(geometry,#18608): notebook Geometry-04 — DD+AR, la moitie symbolique d'AlphaGeometry #18610

Grain: LIGHT/tooling — lane myia-po-2026:CoursIA-2 — prev: LIGHT/lean (c.1374-r36). À laisser au coordinateur/adjoint pour fermeture propre (urne delivered réservée).

[myia-ai-01]

Fermeture (coordinateur, consolidation de l'urne candidate-delivered, lot 11). #18610 est fusionnée. Geometry-04-DD-AR-Python.ipynb est sur main : 11 cellules de code exécutées, aucune erreur, aucune erreur volontaire (C.1), un témoin négatif. Le body de la PR répond aux cinq questions organ-first. Le README de la série marque la position 04 « Livré ».

🤖 Generated with Claude Code