Skip to content

[Epic] Serie SymbolicAI/Geometry — preuve automatique en geometrie, programme gradue (01 figure->equation, 02 Grobner, 03 Wu, 04 DD+AR, 05 pont Lean) #17544

Open
Open
[Epic] Serie SymbolicAI/Geometry — preuve automatique en geometrie, programme gradue (01 figure->equation, 02 Grobner, 03 Wu, 04 DD+AR, 05 pont Lean)#17544
Labels
enhancementNew feature or request

Description

@myia-ai-01
myia-ai-01
opened on Sep 23, 2026

État mesuré au 2026-10-05 (lane myia-po-2025:CoursIA-2, consolidation #13906). La série est livrée de 01 à 04 sur main : première volée 01→03 mergée dans la fenêtre 24-25/09 (#17581, #17588, #17511 — la règle « merger 01-03 ensemble » tenue dans son esprit, trois PRs en 48 h), puis #18610 (01/10) a livré l'accrétion 03b (décomposition de Ritt) et le principal 04 (DD+AR), et #18963 (04/10) a posé le pont 05 : lake geometry_lean (squelette + MidpointHypotenuse.lean + workflow CI lean-geometry.yml, tranche 2 de #18601). L'arbre porte 5 carnets + le lake ; aucune PR Geometry ouverte. Le renommage exigé de Geometry-1-Wu-Method en Geometry-03-... est fait (#17511 mergée sous son nom final). Le body disait « lake de la série Lean, pas de nouveau lake sans motif » : un lake dédié geometry_lean existe désormais, mandaté par #18601 — le motif y est consigné.

Front actuel : tranches suivantes de #18601 (pont 05 — énoncé Lean du théorème fil rouge) ; 02b saturation/Rabinowitsch non vérifié (le titre de #17588 mentionne la saturation, possiblement absorbée par 02 — non mesuré ici). Portée non vérifiée : les critères de review 1-7 (pré-requis, témoin négatif, 3 exercices, organ-first) n'ont pas été re-mesurés carnet par carnet — l'arbre et les fusions seulement. EPIC vivante, non fermable.

Série SymbolicAI/Geometry : la preuve automatique en géométrie, de la figure à la preuve

Epic parapluie demandé par le user sur #17504 (Concern du 23/09 à 09:35Z) : une nouvelle série ne naît pas d'un seul notebook, il lui faut un Epic et un vrai programme. Le user accepte la série (23/09) et me confie son cadrage. Rattachement : piste « Solveurs et calcul » de See #14468.

Pourquoi un cadrage strict dès le premier notebook. La série Complexity est partie de résultats de recherche sans socle, et elle est aujourd'hui « franchement indigeste » (#17045, #17151, refonte en cours sur #17063). Geometry ne refait pas ce chemin. Alourdir l'arbre des séries n'est pas anodin : une nouvelle série doit avoir une progression et une pédagogie impeccables dès sa première PR mergée.

Programme : chemin principal (numéros nus) et accrétions

Pos. Notebook principal Public Suppose Organe réutilisé Accrétion b
01 De la figure à l'équation : coordonnées, hypothèses et conclusion en polynômes, vérification numérique sur des figures tirées au hasard, et pourquoi ce n'est pas une preuve (Schwartz–Zippel donne une preuve probabiliste) Découverte géométrie du lycée, Python de base sympy (polynômes), numpy —
02 Prouver par l'algèbre : idéal engendré par les hypothèses, appartenance, bases de Gröbner, conditions de non-dégénérescence (pourquoi un théorème « vrai » échoue sur une figure dégénérée) Licence 01 sympy.groebner (pas de réimplémentation) 02b : saturation et astuce de Rabinowitsch, si le 02 grossit
03 La méthode de Wu : pseudo-division, ensemble caractéristique, reste nul ; Wu face à Gröbner, sur les mêmes théorèmes que 02 Licence 02 sympy.prem en contre-vérification de la pseudo-division from scratch 03b : décomposition de Ritt, papillon, corpus historique de Chou
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 Licence 01, 03 à qualifier (organ-first) : moteur de règles d'une autre série (Planners, SemanticWeb), sinon copie pédagogique déclarée 04b : IMO-AG-30, Sinha et al. 2024 (Wu associé à DD+AR), proposeur neuronal
05 Pont formel : un théorème de 02 ou 03 énoncé et prouvé dans Lean/Mathlib, et la question de ce que « prouvé par Gröbner » garantit Recherche 02 ou 03, bases de la série Lean lake de la série Lean (pas de nouveau lake sans motif) —

Les règles de fabrication sont des critères de review. Elles ne se renégocient pas notebook par notebook.

  1. Chaque principal ne suppose que ce qui le précède. Il s'ouvre sur « Ce que ce notebook suppose » et porte une étiquette de public.
  2. Aucun résultat de recherche sur le chemin principal. Benchmarks, preprints, comparaisons au niveau IMO et chronologie historique vont en b. Un principal se lit sans ouvrir de lettre.
  3. Un théorème fil rouge traverse 01 à 03. Par exemple, le milieu de l'hypoténuse équidistant, puis Ceva. On le vérifie numériquement en 01, on le prouve par Gröbner en 02, puis par Wu en 03. L'étudiant voit trois regards sur le même objet, pas trois objets.
  4. Un témoin négatif par notebook : un énoncé faux, rejeté par la méthode du notebook.
  5. Trois exercices par principal, avec stubs non bloquants (C.1). Exécution de bout en bout avec sorties (C.2), sur CPU, en moins d'une minute par notebook.
  6. Organ-first : les cinq questions dans le body de chaque PR. Une réimplémentation se déclare comme « copie pédagogique déclarée » quand l'implémentation est le didacticiel, comme la pseudo-division en 03.
  7. README de série avec la gradation visible. La série est ajoutée à SymbolicAI/README.md, audit du fichier entier compris (SymbolicAI/README.md : integrer la serie Geometry (ree-audit fichier-entier) #17510).

Livraison

Hors périmètre

  • Le raisonnement neuronal (proposeur de constructions façon AlphaGeometry) n'entre qu'en accrétion, et seulement s'il est exécutable sur CPU de façon bornée.
  • Aucune nouvelle dépendance lourde sans verdict SOTA écrit.

Activity

  1. myia-ai-01
    added
    enhancementNew feature or request
    on Sep 23, 2026

  2. myia-ai-01 commented on Sep 23, 2026

    @myia-ai-01
    myia-ai-01
    on Sep 23, 2026
    CollaboratorAuthor

    [CLAIMED] lane myia-po-2027:CoursIA — premiere volee de la serie Geometry (01, 02, et 03 = reprise de #17511), posee au dispatch par ai-01 -- paths: MyIA.AI.Notebooks/SymbolicAI/Geometry/**

  3. jsboige
    added 3 commits that reference this issue on Sep 23, 2026

    feat(geometry,#17544): notebook 01 - de la figure a l'equation + READ…

    5843585

    fix(geometry,#17544): Geometry-01 -- protocole Schwartz-Zippel appliq…

    42a1d4e

    Fix: Geometry-02 — liens serie (README.md, Geometry-01) repointes ver…

    e3ec903
  4. myia-ai-01
    added a commit that references this issue on Sep 24, 2026

    feat(geometry,#17544): Geometry 01 — De la figure à l'équation (Décou…

    3dddfd5

  5. jsboige commented on Sep 24, 2026

    @jsboige
    jsboige
    on Sep 24, 2026
    Owner

    [GRAIN-DEEPQUEUE] c.815 — sous-grain "repointer les liens cell.0 du notebook Geometry-02 vers Geometry-01.ipynb et README.md" — déclenché après livraison complète de la série Geometry (#17581 mergé + autres tranches éventuelles). Lane porteuse d'origine : po-2027.

  6. jsboige
    added 2 commits that reference this issue on Sep 24, 2026

    Merge origin/main — conflit Geometry/README.md résolu (programme #17544…

    6360fbc

    Fix: Geometry-02 — liens de série repointés vers les fichiers réels (…

    343c828

  7. jsboige commented on Sep 24, 2026

    @jsboige
    jsboige
    on Sep 24, 2026
    Owner

    [CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Geometry/Geometry-03b-Ritt-Decomposition.ipynb, MyIA.AI.Notebooks/SymbolicAI/Geometry/README.md

    Sous-grain 03b (accrétion de recherche de la 3e étape) : la décomposition de Ritt, le papillon et la correction de l'attribution Sinha. Le papillon et la décomposition vivent aujourd'hui dans #17511 (§10-11) et doivent en sortir — l'élagage de 03 vient après, sur la branche de #17511.

  8. jsboige
    added a commit that references this issue on Sep 24, 2026

    feat(geometry,#17544): le papillon et Ritt partent en 03b ; attributi…

    cbc386c

  9. jsboige commented on Sep 24, 2026

    @jsboige
    jsboige
    on Sep 24, 2026
    Owner

    [INFO] Sous-grain « deplacer le papillon et la decomposition de Ritt vers 03b + corriger l'attribution Sinha » — livre (lane myia-po-2027:CoursIA)

    Porte par #17511, la PR que l'Epic retenait jusque-la : le deplacement est sa condition de deblocage, donc il vit sur sa branche. Tete cbc386c6398a.

    avant apres
    03 41 cellules (24 code) : papillon en §10-11 + exercice 3 33 cellules (19 code) — §10-11 et exercice 3 retires, §12 renumerote §10, pointeurs vers l'accretion
    03b — 32 cellules (15 code) — le papillon et Ritt, developpes et mesures

    Le materiel change de lettre et gagne une mesure (il n'est pas perdu) : 8 cellules retirees du 03 (8272 caracteres de source) ; sorties perdues 1339 caracteres, entierement portees par ces cellules — les 19 cellules conservees en gagnent 86 ; 03 re-execute, execution_count 1-19 contigus, 0 erreur.

    Trois resultats que le 03 enonçait en prose sont desormais mesures dans 03b : la conclusion est un quotient ($g_2 = x_X(b_2-c_2) + y_Y(d_2-a_2)$, verifie par assert) ; les initiales de CS(T2) sont toutes irreductibles — la scission de Ritt ne s'y declenche pas ; sur le bord degenere l'enonce est muet et non faux.

    Attribution Sinha : mesure sur le PDF archive (20188 caracteres extraits) — le mot « Ritt » y est absent (0 occurrence), et le 21/30 vient des methodes synthetiques DD+AR (deductive databases, angle, ratio and distance chasing). La formule « decomposition de Ritt et rejet angulaire (DD+AR) » etait fausse sur ses deux termes ; corrigee dans les deux notebooks et dans le README de serie (ligne 03b livree, ligne 03 corrigee).

    Verifications : check_notebook_navlinks.py 0 casse sur 1395 ; check_cost_metadata.py sans finding ; C.1/C.2/H.1 verts (exec_count contigus 1-19 et 1-15, 0 erreur) ; pre-commit H.3 + gitleaks passes.

    Reste, hors lane : une re-review au nouveau head — la review Hermes portait sur 17d7f2a4, soit le 03 avant le deplacement, elle est superseded ; et la reserve BOT-CONCERN de jsboige (23/09) ne se leve que par son auteur ou par arbitrage ai-01 (une reponse d'auteur ne leve pas une reserve d'un tiers).

  10. myia-ai-01
    added 2 commits that reference this issue on Sep 25, 2026

    feat(geometry,#17544): notebook Geometry-02 -- preuve par algebre (id…

    2b9134b

    feat(geometry,#17544): Geometry 03 — la méthode de Wu (ensembles cara…

    1d06723

  11. jsboige commented on Sep 30, 2026

    @jsboige
    jsboige
    on Sep 30, 2026
    Owner

    Issue fille de qualification pour la position 04 (DD+AR) : #18608 — investigation organ-first pre-remplie (SW-13 owlrl mesure firsthand, recommandation copie pedagogique declaree moteur DD + sympy pour AR). La volée 01-03 etant merger et le re-parenting en cours (#18607), la position 04 est le prochain principal du programme.

  12. myia-ai-01
    added a commit that references this issue on Oct 4, 2026

    feat(lean,#18601): lake geometry_lean — squelette + théorème du milie…

    8179dd7

  13. jsboige commented on Oct 7, 2026

    @jsboige
    jsboige
    on Oct 7, 2026
    Owner

    [CLAIMED] lane myia-po-2025:CoursIA -- dispatch coordinateur ai-01 (file profonde du 07/10) : position suivante du programme gradue Geometry, en partant de la fille de qualification #18608 (04 DD+AR).

  14. jsboige commented on Oct 9, 2026

    @jsboige
    jsboige
    on Oct 9, 2026
    Owner

    [CLAIMED] lane myia-po-2025:CoursIA -- chemin principal #17544, position 05 (pont formel : un theoreme de 02/03 enonce et prouve en Lean, et ce que « prouve par Grobner » garantit). Le lac geometry_lean et son CI sont livres (tranche 2 de #18601, #18963) ; ma tranche 3 (escalier, PR #19705) est mergee. Le carnet Python 05 reste a ecrire -- il lit les enonces du lac par lecture de source, sans build (le pattern etabli par Lean-38).

    Hypothese consignee (mode autonome, CLAUDE.md principe 1) : le programme demande une « issue fille qui qualifie son organe » pour 04 et 05. Aucune issue 05 n'existe, et l'organe de 05 est deja qualifie -- sympy.groebner est celui de 02/03, sans reimplementation, et la lecture du lac est le pattern de Lean-38. Les 5 questions organ-first sont donc portees par le body de la PR au lieu d'une issue fille.

    Claim pose avant la premiere edition (lane-claim-protocol, check_lane_claim 17544 : CLEAR, reprise de mon propre claim).

    paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Geometry/**, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md, MyIA.AI.Notebooks/SymbolicAI/README.md

  15. jsboige
    added 2 commits that reference this issue on Oct 9, 2026

    Fix(geometry,#17544): corrige le renvoi relatif vers Lean-38 dans Geo…

    9238a74

    fix(geometry,#17544): mailler la chaine de navigation 02->03 et 04->05

    a6920aa
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions