Geometry 04 — Raisonner comme un géomètre (DD + AR)

Public : Licence — quatrième notebook de la série Geometry, le programme gradué de la preuve automatique en géométrie ; il suppose la lecture de 01 (De la figure à l’équation) et de 03 (La méthode de Wu).

Ce que ce notebook suppose. Les prédicats géométriques et leur traduction polynomiale (01), l’idée qu’une méthode de preuve produit une garantie vérifiable (02, 03), et le Python de base (tuples, ensembles, fonctions d’ordre supérieur). Aucune connaissance d’AlphaGeometry n’est requise : le notebook la construit.

En 2024, le système AlphaGeometry (Trinh et al., Solving olympiad geometry without human demonstrations) résout des problèmes de géométrie de niveau olympiades sans aucun exemple humain. Sa moitié symbolique — la seule que ce notebook construit — n’est ni Gröbner (02), ni Wu (03) : c’est un duo inédit dans la série :

DD (Deductive Database) : une base de faits géométriques close sous un corpus de règles élémentaires — la machine raconte comme un géomètre, chaque fait dérivé portant sa chaîne de règles ;
AR (Algebraic Reasoning) : la traduction polynomiale de 01/02 réutilisée comme oracle — la machine calcule ce que les règles ne joignent pas.

Le fil rouge de la série (le milieu de l’hypoténuse équidistant des trois sommets) reçoit ici son quatrième regard — et ce regard a une surprise : DD, laissé seul, échoue sur le théorème le plus simple de la série. Comprendre pourquoi est exactement comprendre ce que AlphaGeometry ajoute aux règles.

§1. Une base de déduction : des faits, des règles, une fermeture

Un fait est un tuple (nom, *points) : ("midp", "M", "B", "C") dit que M est le milieu de [BC], ("cong", "A", "M", "B", "M") que AM = BM, ("perp", "B", "A", "C", "A") que les droites (AB) et (AC) sont perpendiculaires. La géométrie est symétrique — AM = BM se lit aussi BM = AM — donc chaque fait possède une forme canonique : toutes les écritures équivalentes d’un même énoncé tombent sur le même tuple, et la base peut être un simple dictionnaire.

from itertools import combinations

def canon(fact):
    """Forme canonique d'un fait : les symetries d'arguments ne creent pas de fait nouveau."""
    name, args = fact[0], fact[1:]
    if name == "cong":                      # |AB| = |CD| : aretes non orientees, paire non ordonnee
        e1, e2 = tuple(sorted(args[:2])), tuple(sorted(args[2:]))
        lo, hi = sorted((e1, e2))
        return ("cong",) + lo + hi
    if name == "coll":                      # alignement : 3 points non ordonnes
        return ("coll",) + tuple(sorted(args))
    if name in ("perp", "para"):            # droites non orientees, paire non ordonnee
        l1, l2 = tuple(sorted(args[:2])), tuple(sorted(args[2:]))
        lo, hi = sorted((l1, l2))
        return (name,) + lo + hi
    if name == "midp":                      # M milieu de [AB] : [AB] non oriente
        return ("midp", args[0]) + tuple(sorted(args[1:]))
    return fact

def pretty(fact):
    """Rendu lisible d'un fait canonique."""
    name, a = fact[0], fact[1:]
    if name == "cong":
        return f"|{a[0]}{a[1]}| = |{a[2]}{a[3]}|"
    if name == "coll":
        return f"{a[0]}, {a[1]}, {a[2]} alignes"
    if name == "perp":
        return f"({a[0]}{a[1]}) _|_ ({a[2]}{a[3]})"
    if name == "para":
        return f"({a[0]}{a[1]}) // ({a[2]}{a[3]})"
    if name == "midp":
        return f"{a[0]} milieu de [{a[1]}{a[2]}]"
    return str(fact)

# verifions les symetries sur un exemple : toutes ces ecritures donnent le meme fait
variants = [("cong","A","M","B","M"), ("cong","M","A","M","B"), ("cong","B","M","A","M"), ("cong","M","B","M","A")]
print({pretty(canon(v)) for v in variants})
print("1 seul fait canonique :", len({canon(v) for v in variants}) == 1)

{'|AM| = |BM|'}
1 seul fait canonique : True

Une règle est une fonction qui regarde la base et propose de nouveaux faits. Le corpus ci-dessous est volontairement élémentaire — cinq règles qu’un élève de lycée reconnaît :

Règle	Énoncé	Nature
`midp_def`	M milieu de [AB] ⇒ AM = MB	définition
`midp_coll`	M milieu de [AB] ⇒ A, M, B alignés	définition
`cong_trans`	AB = CD et CD = EF ⇒ AB = EF	transitivité
`perp_para`	deux perpendiculaires à une même droite ⇒ parallèles	propriété de l’angle droit
`coll_perp`	l’alignement propage la perpendicularité	substitution de points

def rule_midp_def(base):
    """midp(M,A,B) -> cong(A,M,M,B) : les deux moities d'un meme segment sont egales."""
    out = {}
    for f in base:
        if f[0] == "midp":
            m, a, b = f[1], f[2], f[3]
            out[canon(("cong", a, m, m, b))] = ("midp_def", (f,))
    return out

def rule_midp_coll(base):
    """midp(M,A,B) -> coll(A,M,B) : le milieu est sur le segment."""
    out = {}
    for f in base:
        if f[0] == "midp":
            m, a, b = f[1], f[2], f[3]
            out[canon(("coll", a, m, b))] = ("midp_coll", (f,))
    return out

def rule_cong_trans(base):
    """cong(A,B,C,D) et cong(C,D,E,F) -> cong(A,B,E,F) : transitivite des longueurs."""
    out = {}
    by_edge = {}
    for f in base:
        if f[0] == "cong":
            e1, e2 = (f[1], f[2]), (f[3], f[4])
            by_edge.setdefault(e1, set()).add((f, e2))
            by_edge.setdefault(e2, set()).add((f, e1))
    for e, voisins in by_edge.items():
        for f1, e2 in voisins:
            for f2, e3 in by_edge.get(e2, ()):
                if e3 != e:
                    out[canon(("cong",) + e + e3)] = ("cong_trans", (f1, f2))
    return out

def rule_perp_para(base):
    """perp(l1,l2) et perp(l1,l3) -> para(l2,l3) : deux perpendiculaires a une meme droite sont paralleles."""
    out = {}
    perps = [f for f in base if f[0] == "perp"]
    for f1 in perps:
        l1, l2 = (f1[1], f1[2]), (f1[3], f1[4])
        for f2 in perps:
            l3, l4 = (f2[1], f2[2]), (f2[3], f2[4])
            if l1 == l3 and l2 != l4:
                out[canon(("para",) + l2 + l4)] = ("perp_para", (f1, f2))
            if l1 == l4 and l2 != l3:
                out[canon(("para",) + l2 + l3)] = ("perp_para", (f1, f2))
    return out

def rule_coll_perp(base):
    """coll(A,B,C) et perp(A,B,l) -> perp(C,B,l) : remplacer un point par un point aligne."""
    out = {}
    for fc in (f for f in base if f[0] == "coll"):
        pts = set(fc[1:])
        for fp in (f for f in base if f[0] == "perp"):
            for i, j in ((1, 2), (3, 4)):
                p, q = fp[i], fp[j]
                if p in pts and q in pts:
                    for r in pts - {p, q}:
                        new = tuple(sorted((r, q)))
                        other = tuple(sorted((fp[3], fp[4]) if i == 1 else (fp[1], fp[2])))
                        lo, hi = sorted((new, other))
                        out[("perp",) + lo + hi] = ("coll_perp", (fc, fp))
    return out

RULES = [rule_midp_def, rule_midp_coll, rule_cong_trans, rule_perp_para, rule_coll_perp]
print(f"corpus : {len(RULES)} regles elementaires")

corpus : 5 regles elementaires

Le moteur est une fermeture : on applique toutes les règles jusqu’à ce qu’aucun fait nouveau n’apparaisse (point fixe). La nouveauté pédagogique — c’est elle qui distingue DD d’un simple solveur — est la trace de preuve : chaque fait dérivé retient la règle qui l’a produit et les faits parents. La preuve n’est plus un saut no man’s land de l’hypothèse à la conclusion : c’est une chaîne qu’on peut remonter et lire.

def closure(facts, rules, max_rounds=20):
    """Forward chaining jusqu'au point fixe.

    Renvoie (base, rounds) où base[fait] = (règle, faits parents) ;
    les faits initiaux portent la regle 'hypothese'.
    """
    base = {canon(f): ("hypothese", ()) for f in facts}
    rounds = 0
    changed = True
    while changed and rounds < max_rounds:
        changed = False
        rounds += 1
        for rule in rules:
            for fact, (rname, parents) in rule(base).items():
                if fact not in base:
                    base[fact] = (rule.__name__.replace("rule_", ""), parents)
                    changed = True
    return base, rounds

def proof_chain(base, fact):
    """Remonte la chaine de preuve d'un fait : (regle, fait, parents) jusqu'aux hypotheses."""
    chain, seen, stack = [], set(), [fact]
    while stack:
        f = stack.pop()
        if f in seen:
            continue
        seen.add(f)
        rname, parents = base[f]
        chain.append((rname, f, parents))
        stack.extend(parents)
    return chain

print("moteur DD pret : closure() + proof_chain()")

moteur DD pret : closure() + proof_chain()

§2. Le fil rouge, quatrième regard — et un échec instructif

Le théorème : dans un triangle ABC rectangle en A, le milieu M de l’hypoténuse [BC] est équidistant des trois sommets. En prédicats, l’hypothèse et la cible :

Hypothèses : (BA) ⊥ (CA) et M milieu de [BC] ;
Cible : MA = MB et MA = MC (le fait MB = MC, lui, n’est que la définition du milieu).

Lançons la fermeture et regardons tout ce que DD sait faire sur ce théorème.

hypotheses = [
    ("perp", "B", "A", "C", "A"),   # (BA) _|_ (CA) : angle droit en A
    ("midp", "M", "B", "C"),        # M milieu de l'hypotenuse [BC]
]

base, rounds = closure(hypotheses, RULES)
print(f"fermeture atteinte en {rounds} tours : {len(base)} faits")
for f in sorted(base):
    rname, _ = base[f]
    print(f"  [{rname:10s}] {pretty(f)}")

fermeture atteinte en 2 tours : 4 faits
  [midp_coll ] B, C, M alignes
  [midp_def  ] |BM| = |CM|
  [hypothese ] M milieu de [BC]
  [hypothese ] (AB) _|_ (AC)

Lecture du résultat

La fermeture est… maigre. DD dérive correctement le combinatoire : BM = CM (définition du milieu) et l’alignement de B, M, C. Mais la cible :

MA = MB : absent ;
MA = MC : absent.

Ce n’est pas un bug du moteur — c’est une limite de principe, et elle est le cœur de ce notebook. La preuve synthétique classique du théorème construit un point auxiliaire (le symétrique de A par rapport à M, ou le cercle de diamètre [BC]) : elle ajoute un objet au monde. Or une base de déduction ne fait qu’exploiter les objets déjà présents — sur nos quatre points A, B, C, M, aucune chaîne de règles élémentaires ne joint MA à MB. C’est précisément pourquoi AlphaGeometry adjoint à DD un proposeur de constructions (neuronal chez lui) : quelqu’un doit agrandir le monde.

La deuxième réponse, celle que ce notebook explore, est de changer d’arithmétique : si les règles ne joignent pas MA et MB, l’algèbre, elle, sait.

cibles = {
    "MA = MB": canon(("cong", "M", "A", "M", "B")),
    "MA = MC": canon(("cong", "M", "A", "M", "C")),
    "MB = MC": canon(("cong", "M", "B", "M", "C")),
}
for label, fact in cibles.items():
    statut = "DERIVE par DD" if fact in base else "ABSENT de DD"
    print(f"{label:8s} : {statut}")

MA = MB  : ABSENT de DD
MA = MC  : ABSENT de DD
MB = MC  : DERIVE par DD

§3. AR : l’algèbre en renfort, avec l’outillage de 01 et 02

Le raisonnement algébrique de AlphaGeometry traduit l’énoncé en équations — exactement le geste du notebook 01 — puis les combine. Nous réutilisons l’organe de la série, sympy (et sa base de Gröbner rencontrée en 02), sans rien réimplémenter :

l’angle droit en A s’écrit \((\vec{AB} \cdot \vec{AC}) = 0\) ;
le milieu s’écrit \(M = \frac{B+C}{2}\), coordonnée par coordonnée.

La cible \(MA^2 = MB^2\) est prouvée si le polynôme \(MA^2 - MB^2\) se réduit à zéro modulo les hypothèses.

import sympy as sp

# A=(xa,ya), B=(0,0) origine, C=(xc,yc), M=(xm,ym) : quatre inconnues suffisent
xa, ya, xc, yc, xm, ym = sp.symbols("xa ya xc yc xm ym", real=True)

hyp_perp   = xa * (xc - xa) + ya * (yc - ya)      # (BA).(CA) = 0
hyp_mid_x  = xm - xc / 2                          # M = (B+C)/2, abscisse
hyp_mid_y  = ym - yc / 2                          # M = (B+C)/2, ordonnee

G = sp.groebner([hyp_perp, hyp_mid_x, hyp_mid_y], xm, ym, xc, yc, xa, ya, order="lex")
print("base de Groebner des hypotheses : ok,", len(G.polys), "polynomes")

base de Groebner des hypotheses : ok, 3 polynomes

def ar_prove(cible):
    """Prouve cible (polynome) modulo les hypotheses : reduction a zero par la base de Groebner."""
    _coeffs, residu = G.reduce(sp.expand(cible))
    return residu == 0

MA2 = (xm - xa)**2 + (ym - ya)**2
MB2 = xm**2 + ym**2
MC2 = (xm - xc)**2 + (ym - yc)**2

for label, poly in {"MA^2 - MB^2": MA2 - MB2, "MA^2 - MC^2": MA2 - MC2}.items():
    print(f"{label:14s} : {'PROUVE par AR (residu nul)' if ar_prove(poly) else 'residu NON NUL'}")

MA^2 - MB^2    : PROUVE par AR (residu nul)
MA^2 - MC^2    : PROUVE par AR (residu nul)

Lecture du résultat

Le duo fonctionne : là où DD s’arrête, AR prouve les deux égalités par simple réduction à zéro. Notez la division du travail exacte de AlphaGeometry :

	DD	AR
Ce qu’il prouve	les faits combinatoires (alignements, moitiés, parallèles)	les relations métriques (distances, rapports)
La preuve est…	lisible : une chaîne de règles qu’un humain relit	calculée : une réduction modulo un idéal
Ce qu’il exige	un corpus de règles, des objets déjà construits	des coordonnées, un solveur polynomial

Ce partage n’est pas une commodité d’implémentation : dans AlphaGeometry, il faut les deux, car chacun couvre l’angle mort de l’autre — DD ne rejoint pas le métrique sans construction, AR ne dit rien du combinatoire lisible.

§4. Témoin négatif : un énoncé faux, rejeté deux fois

La règle de fabrication de la série exige un ténoncé faux que la méthode rejette. Prenons : la médiane issue de l’angle droit vaut le quart de l’hypoténuse, c’est-à-dire \(MA = \frac{MB}{4}\). DD ne le dérive pas (il n’est nulle part dans la fermeture — bonne nouvelle) mais un moteur qui échoue silencieusement n’est pas un témoin : c’est AR qui transforme l’absence en réfutation, avec un résidu non nul mesuré.

# Enonce faux : MA^2 = MB^2 / 16  (soit MA = MB/4)
enonce_faux = MA2 - MB2 / 16
_coeff, residu = G.reduce(sp.expand(enonce_faux))
print("residu de MA^2 - MB^2/16 modulo les hypotheses :")
print(" ", sp.nsimplify(residu))
print("verdict AR :", "RESIDU NON NUL -> enonce REJETE" if residu != 0 else "residu nul ?!")
print("verdict DD :", "absent de la fermeture (jamais derive)")

residu de MA^2 - MB^2/16 modulo les hypotheses :
  15*xc**2/64 + 15*yc**2/64
verdict AR : RESIDU NON NUL -> enonce REJETE
verdict DD : absent de la fermeture (jamais derive)

Lecture du résultat

Le rejet est double : DD ne dérive jamais l’énoncé faux (il n’est pas conséquence combinatoire des règles), et AR produit un résidu explicitement non nul — l’énoncé est incompatible avec les hypothèses, pas simplement hors d’atteinte. C’est la différence entre je ne sais pas le prouver et c’est faux : une base de déduction seule ne fait pas la différence, le duo la fait.

Une remarque d’honnêteté : un résidu non nul à la réduction ne prouve la fausseté que sur la composante non dégénérée — le même genre de précaution que les conditions de non-dégénérescence de 02 et 03. Lisons le résidu : \(\frac{15}{64}(x_c^2 + y_c^2)\) ne s’annule que si C = B — une figure dégénérée d’hypoténuse nulle. Sur toute figure non dégénérée (C ≠ B), l’énoncé faux est bien réfuté ; et c’est une réfutation plus forte qu’un simple échec de preuve.

§5. Ce que le quatrième regard a appris

Le tableau des quatre regards sur le même théorème :

Notebook	Regard	Ce qu’il garantit
01	numérique (Schwartz-Zippel)	vrai avec grande probabilité sur figures tirées au hasard
02	algébrique (Gröbner)	vrai exactement, conditions de non-dégénérescence explicites
03	algorithmique (Wu)	vrai exactement, non-dégénérescences produites par l’élimination
04	hybride (DD + AR)	vrai exactement, avec preuve combinatoire lisible et réfutation mesurée

AlphaGeometry complète ce tableau par la suite : DD+AR y est couplé à un proposeur neuronal de constructions (le point auxiliaire qui manquait au §2), ce qui est l’objet de l’accrétion 04b (IMO-AG-30) — hors chemin principal.

Exercices

Les trois exercices étendent le corpus ou la chaîne de preuve. Ils sont à compléter ; le notebook doit s’exécuter de bout en bout même non complété.

# Exercice 1 — Elargir le corpus.
# Ajoutez une regle rule_coll_trans : si A,B,C sont alignes et A,B,D aussi,
# alors A,C,D sont alignes (transitivite de l'alignement). Relancez la fermeture
# du fil rouge avec le corpus etendu et affichez le nombre de faits nouveaux.
# TODO etudiant
# Indice : parcourez les faits "coll" de la base ; deux faits partageant deux points
#   donnent un troisieme alignement parmi les points restants (canon() deduplique).
# Etape 1 : ecrire rule_coll_trans(base) sur le modele des regles existantes.
# Etape 2 : RULES_EXT = RULES + [rule_coll_trans] puis closure(hypotheses, RULES_EXT).
print("Exercice a completer")

Exercice a completer

# Exercice 2 — Lire une preuve DD.
# Affichez la chaine de preuve complete du fait BM = CM dans la base du fil rouge
# (fonction proof_chain), puis reecrivez-la en une phrase Francaise du genre
# "BM = CM car M est le milieu de [BC], hypothese du probleme".
# TODO etudiant
# Indice : proof_chain(base, canon(("cong", "M", "B", "M", "C"))) retourne une liste
#   de (regle, fait, parents) ; pretty(fait) rend chaque fait lisible.
# Etape 1 : recuperer la chaine. Etape 2 : l'afficher ligne par ligne.
print("Exercice a completer")

Exercice a completer

# Exercice 3 — Refuter par AR.
# Testez l'enonce : "la mediane issue de l'angle droit vaut le TIERS de la demi-hypotenuse",
# soit MA^2 = MB^2 / 9. Refutez-le par reduction, puis verifiez au passage que
# l'enonce correct MA^2 = MB^2 reste prouve (residu nul).
# TODO etudiant
# Indice : meme geste que le temoin negatif du 4 : G.reduce(sp.expand(MA2 - MB2/9)).
# Etape 1 : reduire MA2 - MB2/9. Etape 2 : conclure sur le verdict (residu nul ou non).
print("Exercice a completer")

Exercice a completer

Conclusion

Ce notebook a construit la moitié symbolique de AlphaGeometry et l’a confrontée au fil rouge de la série :

Brique	Rôle	Où
`canon` / `pretty`	faits géométriques sous forme canonique, symétries neutralisées	§1
corpus de 5 règles	les gestes élémentaires du géomètre	§1
`closure` / `proof_chain`	fermeture à point fixe, preuve lisible remontable	§1
l’échec de DD	le métrique sans construction est hors d’atteinte — la limite de principe	§2
AR (`sympy.groebner`)	l’oracle polynomial de 01/02 réutilisé, réduction à zéro	§3
témoin négatif	absence (DD) + résidu non nul (AR) = réfutation, pas seulement échec	§4

La série poursuit : 04b (IMO-AG-30, le proposeur neuronal couplé à DD+AR) en accrétion, et 05 (un théorème de la série énoncé et prouvé en Lean/Mathlib — que garantit « prouvé par Gröbner » ?) au bout du programme gradué.

Retour au sommet