from sympy import symbols, Poly, prem, expand, groebner, factor, Rational, sqrt, solve, nsimplify
import time
import sympy
print("sympy", sympy.__version__)sympy 1.14.0Geometry 03 — La méthode de Wu
Public : Licence — troisiè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 02 (From Equation to Proof).
En 1977, le mathématicien chinois Wen-tsün Wu introduit un algorithme capable de démontrer automatiquement des théorèmes de géométrie élémentaire — des centaines d’énoncés classiques de la littérature, dont certains que personne n’avait formalisés depuis des siècles. La méthode traduit chaque théorème en un système polynomial, puis le prouve par une élimination algébrique systématique : la division pseudo-polynomiale le long d’un ensemble caractéristique.
Cette approche a connu en 2024 un retour spectaculaire : l’étude Wu’s Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry (Sinha et al., arXiv:2404.06405) montre que la méthode de Wu seule, sur un laptop portable (AMD Ryzen 7, 16 Go, 5 min par problème), résout 15/30 problèmes de la passerelle IMO-AG-30 — dont deux problèmes (IMO 2021 P3, IMO 2008 P1B) qu’aucun des systèmes neuro-symboliques évalués ne résout. Combinée aux méthodes synthétiques classiques DD+AR — deductive databases et angle, ratio and distance chasing — elle atteint 21/30, niveau médaille d’argent, et combinée à AlphaGeometry elle porte le SOTA à 27/30 (or).
Ce notebook construit la méthode à partir de zéro : pseudo-reste, ensemble caractéristique, test de Wu, conditions de non-dégénérescence auto-générées — puis confronte chaque preuve à une vérification indépendante par bases de Gröbner. Le cas limite où cette version simplifiée devient non-concluante — le théorème du papillon, dont la variété est réductible — est traité par l’accrétion de recherche Geometry-03b, qui implémente la décomposition de Ritt et mesure ce qu’elle y donne.
Objectifs pédagogiques
- Traduire un théorème géométrique en hypothèses et conclusion polynomiales sur ℚ (choix de repère, paramètres vs inconnues).
- Implémenter le pseudo-reste
premet le confronter àsympy.prem. - Construire un ensemble caractéristique par l’algorithme de basic-set de Chou.
- Prouver deux théorèmes (milieu de l’hypoténuse, Ceva) par le test de Wu, et extraire les conditions de non-dégénérescence qu’il produit automatiquement.
- Rejeter un énoncé faux (témoin négatif) et vérifier indépendamment chaque preuve par bases de Gröbner saturées (astuce de Rabinowitsch).
Prérequis : manipulation de polynômes à plusieurs variables, notions d’idéal et de variété algébrique (V(I) = ensemble des zéros communs), bases de Gröbner vues comme outil boîte-noire (la série SMT/Z3 du dépôt couvre le contexte solveur). Aucun prérequis de géométrie avancée.
Référence principale : Shiven Sinha, Ameya Prabhu, Ponnurangam Kumaraguru, Siddharth Bhat, Matthias Bethge, Wu’s Method can Boost Symbolic AI to Rival Silver Medalists and AlphaGeometry to Outperform Gold Medalists at IMO Geometry, 2024, arXiv:2404.06405 — PDF archivé dans le gisement commun (G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\). Historique : Wu (1978), Chou, Mechanical Geometry Theorem Proving (1988), Ritt (1950).
Plan du notebook
| § | Contenu | Livrable |
|---|---|---|
| 1–2 | Traduction géométrie → polynômes, fil rouge T1 | encodage H1, g1 |
| 3 | Pseudo-reste prem |
prem_s, cross-check sympy.prem |
| 4–5 | Chaîne ascendante et test de Wu | basic_set, char_set_basic, wu_prem — preuve de T1 |
| 6–7 | Non-dégénérescences, vérification Gröbner | initials, groebner_sat_verify |
| 8 | Théorème de Ceva | preuve de T3 + conditions auto-générées |
| 9 | Témoin négatif | rejet d’un énoncé faux |
| 10 | Exercices | 2 énoncés à compléter |
Chaque brique algorithmique est implémentée dans le notebook (pas importée d’une librairie) : c’est la manière de comprendre pourquoi ça marche — et le cross-check avec sympy garantit que l’implantation pédagogique est fidèle au moteur de référence.
1. Du théorème géométrique au système polynomial
Le principe fondateur (Descartes → Tarski → Wu) : placés dans un repère, les objets géométriques deviennent des tuples de nombres, les hypothèses (alignement, cyclicité, égalité de longueurs…) deviennent des équations polynomiales, et la conclusion devient un polynôme qui doit s’annuler partout où les hypothèses s’annulent.
Théorème automatiquement prouvable : un couple (H, g) où H = {h₁, …, hₛ} ⊂ ℚ[x₁, …, xₙ] sont les hypothèses et g ∈ ℚ[x₁, …, xₙ] la conclusion. Prouver le théorème = établir que g s’annule sur l’ensemble des solutions de H (à des cas dégénérés près — c’est tout le sujet de ce notebook).
Deux familles d’algorithmes existent :
| Approche | Mécanisme | Coût typique en géométrie |
|---|---|---|
| Bases de Gröbner | réécriture de l’idéal ⟨H⟩ sous ordre d’élimination | exponentiel en le nombre de variables ; les théorèmes de géométrie mélangent paramètres et inconnues, et le calcul explose |
| Méthode de Wu | élimination incrémentale par pseudo-division le long d’une chaîne triangulaire | chaque étape reste polynomiale de degré borné ; des centaines de théorèmes clos en quelques secondes |
L’intuition clef de Wu : un système géométrique est souvent proche d’être triangulaire — si on ordonne bien les variables (les points libres d’abord, les points contraints ensuite), chaque hypothèse détermine « à peu près » une inconnue. La méthode organise H en une chaîne ascendante \(f_1 \prec f_2 \prec \dots \prec f_r\) où chaque \(f_i\) a une variable principale distincte, puis divise la conclusion par cette chaîne — sans jamais diviser dans les coefficients, grâce au pseudo-reste.
Un peu d’histoire. La question « peut-on mécaniser le raisonnement géométrique ? » remonte à Hilbert (ses Grundlagen, 1899, contiennent déjà un critère de décision pour une classe de théorèmes d’incidence) et à Tarski (1951 : la géométrie élémentaire est décidable — par élimination des quantificateurs, hélas inutilisable en pratique). Wu Wen-tsün, formé à la topologie, redécouvre dans les années 70 les ensembles caractéristiques de Ritt (1950, théorie des équations différentielles) et les retourne en un algorithme de démonstration : entre 1977 et 1988, des centaines de théorèmes non triviaux sont ainsi prouvés par machine — dont plusieurs que la littérature n’avait jamais démontrés correctement (Chou raconte le cas de la droite de Morley généralisée : la « preuve » publiée du théorème était fausse, les cas dégénérés tuant l’énoncé tel que formulé). L’article de 2024 referme la boucle : là où les LLM géométriques devinent des constructions, la méthode de Wu certifie — et les deux problèmes IMO qu’elle seule résout dans l’étude sont précisément ceux qui exigent une comptabilité exacte des cas dégénérés.
Le fil rouge du début : le théorème classique « dans un triangle rectangle, le milieu de l’hypoténuse est équidistant des trois sommets ».
Quand la traduction se dégrade — un avertissement : la réduction à des polynômes n’est pas une perte d’information gratuite. Les inégalités (entre > et <) se perdent : « D est sur le segment [BC] » se traduit par la même équation d’alignement que « D sur la droite (BC) », et l’énoncé prouvé est plus fort que le théorème usuel (il couvre les prolongements) ou différent (l’intersection des droites peut tomber loin du segment). Les distances deviennent des carrés (MA² = MB² ne dit rien du signe), les angles deviennent des déterminants (une égalité d’angles au sommet se perd au virage d’un angle obtus). Retenir le principe : on prouve la version polynomiale de l’énoncé — et c’est précisément ce qu’il faudra confronter à l’énoncé géométrique, exercice de lecture critique aux §9-§11.
2. Le fil rouge : milieu de l’hypoténuse (T1)
T1. Soit ABC un triangle rectangle en A, et M le milieu de l’hypoténuse [BC]. Alors MA = MB (et MA = MC).
Choix du repère. La règle d’art : fixer ce qui est libre par isométrie (translations/rotations), paramétrer ce qui reste libre, ne garder comme inconnues que les points contraints.
| Point | Coordonnées | Statut |
|---|---|---|
| A | (0, 0) | fixé (rotation + translation : le sommet de l’angle droit à l’origine, un côté sur l’axe x) |
| B | (u₁, 0) | paramètre (u₁ ≠ 0) |
| C | (0, u₂) | paramètre (u₂ ≠ 0) — l’angle droit en A impose (AB) ⊥ (AC) |
| M | (x_m, y_m) | inconnue — contrainte : milieu de [BC] |
Traduction des hypothèses — « M milieu de [BC] » équivaut à deux équations de coordonnées :
\[h_1 : 2x_m - u_1 = 0 \qquad h_2 : 2y_m - u_2 = 0\]
Traduction de la conclusion — « MA = MB » (les distances au carré, pour rester polynomial) :
\[g : (x_m^2 + y_m^2) - \big((x_m - u_1)^2 + y_m^2\big) = 0\]
Ordre des variables : \(u_1 \prec u_2 \prec x_m \prec y_m\) — les paramètres d’abord (variables à éliminer en dernier), les inconnues ensuite. C’est l’ordre d’élimination de la méthode.
# Encodage de T1
u1, u2, xm, ym = symbols("u1 u2 xm ym")
V1 = [u1, u2, xm, ym] # ordre des variables (parametres, puis inconnues)
h1 = 2*xm - u1 # M_x = (B_x + C_x)/2 = u1/2
h2 = 2*ym - u2 # M_y = u2/2
H1 = [h1, h2]
g1 = (xm**2 + ym**2) - ((xm - u1)**2 + ym**2) # MA^2 - MB^2
print("H =", H1)
print("g =", expand(g1))H = [-u1 + 2*xm, -u2 + 2*ym]
g = -u1**2 + 2*u1*xm# Sanity numerique TOUJOURS avant la machinerie symbolique :
# un triangle concret (u1=4, u2=3 -> M=(2, 3/2)), on evalue hypotheses et conclusion.
cfg = {u1: 4, u2: 3, xm: Rational(2), ym: Rational(3, 2)}
print("h1(cfg) =", h1.subs(cfg), " h2(cfg) =", h2.subs(cfg))
print("g1(cfg) =", g1.subs(cfg), " (attendu : 0)")h1(cfg) = 0 h2(cfg) = 0
g1(cfg) = 0 (attendu : 0)3. Le pseudo-reste prem
La division euclidienne de f par g en la variable v exige de diviser par le coefficient dominant de g. En géométrie, ce coefficient est un polynôme dans les variables restantes — le diviser ferait sortir des polynômes, vers les fractions rationnelles, et perdrait la structure.
Le pseudo-reste contourne : on multiplie f par une puissance suffisante du coefficient dominant \(lc_v(g)\), si bien que chaque étage de la division se fait sans fraction. Formellement, pour \(\deg_v g = d\) et \(\deg_v f = m \geq d\) :
\[lc_v(g)^{m-d+1} \cdot f = q \cdot g + r, \qquad \deg_v r < d\]
et l’algorithme est une boucle de réduction explicite : tant que \(\deg_v r \geq \deg_v g\), remplacer \(r \leftarrow lc \cdot r - lc(r) \cdot v^{\deg_v r - d} \cdot g\). Chaque tour tue le monôme dominant de r en v — le degré en v strictement décroît, d’où la terminaison.
Suivons un tour à la main sur f = x²y + x, g = xy − 3, variable x (lc = y) :
- r = x²y + x : degré 2 en x, monôme dominant x²·y. On forme lc·r − lc(r)·x²⁻¹·g = y·(x²y + x) − (y)·x·(xy − 3) = x²y² + xy − x²y² + 3xy = 4xy.
- r = 4xy : degré 1, dominant 4xy. lc·r − lc(r)·x⁰·g = y·4xy − 4y·(xy − 3) = 4xy² − 4xy² + 12y = 12y.
- r = 12y : degré 0 en x < 1 : stop. prem = 12y — et de fait y²·f = (xy² + 4y)·(xy − 3) + 12y : le facteur y² = lc² est le prix de l’absence de division.
La clef pour la suite : le pseudo-reste multiplie par lc — donc une identité prem(f, g) = r ne vaut que là où lc ≠ 0. Ce détail apparemment technique devient, répété à toute une chaîne, la source des conditions de non-dégénérescence du §6.
def prem_s(f, g, v):
'''Pseudo-reste de f par g en la variable v (implementation pedagogique).
Retourne r tel que lc^(m-d+1) f = q g + r avec deg_v(r) < deg_v(g).
'''
f, g = expand(f), expand(g)
dg = Poly(g, v).degree()
if dg == 0: # g ne depend pas de v : rien a reduire
return f
lc = Poly(g, v).LC() # coefficient dominant (un POLYNOME des autres vars)
r = f
while r != 0 and Poly(r, v).degree() >= dg:
dr = Poly(r, v).degree()
cr = Poly(r, v).LC()
r = expand(lc * r - cr * v**(dr - dg) * g)
return r
# Demon sur un petit cas : f = x^2*y + x, g = x*y - 3, variable x
x, y = symbols("x y")
print("prem_s =", prem_s(x**2*y + x, x*y - 3, x))prem_s = 12*y# Cross-check systematique contre sympy.prem (le moteur de reference) :
# meme convention : prem(f, g, v) est le reste pseudo-division de f par g.
cas = [
(x**3 - 2*x*y + 5, x**2 - y, x),
(y*x**2 + 3*x + 1, x - y, x),
(x**2*y**2 + x*y, x*y + 1, x),
(x**4 + y, x**2 + x*y + 1, x),
(x**3 + y**3 + x, x + y**2, y),
]
for f, g, v in cas:
r_scratch = prem_s(f, g, v)
r_sympy = prem(f, g, v)
assert expand(r_scratch - r_sympy) == 0, (f, g, v, r_scratch, r_sympy)
print(f"Cross-check OK : prem_s == sympy.prem sur {len(cas)} cas")Cross-check OK : prem_s == sympy.prem sur 5 cas4. Ensembles caractéristiques : la chaîne ascendante
La méthode de Wu élimine le long d’une structure triangulaire. Trois définitions :
- Variable principale d’un polynôme f : la plus grande variable (pour l’ordre choisi) qui y apparaît réellement — notée \(mv(f)\). Le polynôme est vu comme polynôme en \(mv(f)\) à coefficients polynomiaux dans les variables plus petites.
- Rang de f : le couple \((\text{indice de } mv(f), \deg_{mv(f)} f)\) — l’ordre lexicographique sur ce couple ordonne les polynômes.
- Chaîne ascendante / ensemble caractéristique : une famille \(f_1 \prec \dots \prec f_r\) dont les variables principales sont deux à deux distinctes et strictement croissantes — une « triangulation » du système, chaque équation déterminant sa variable.
L’algorithme de basic-set (Chou) construit une telle chaîne depuis H par sélection gloutonne : trier H par rang, prendre chaque polynôme dont la variable principale n’est pas encore occupée. Puis l’itération de Chou : réduire tous les polynômes non retenus par pseudo-division à travers la chaîne ; tout reste non nul est ajouté à H (il contraint davantage le système) ; recommencer jusqu’à stabilité. La stabilité signifie : H est impliqué par sa chaîne — la chaîne « porte » le système.
Pourquoi l’itération est nécessaire : deux hypothèses partageant la même variable principale ne déterminent pas forcément la même chose. Exemple : h’ : xm² + u₁ − 1 = 0 et h₁ : 2xm − u₁ = 0 ont toutes deux xm pour variable principale ; la chaîne n’en garde qu’une, et l’autre doit être réduite par elle : prem(h’, h₁, xm) élimine le monôme en xm² et produit un nouveau polynôme — souvent une relation de compatibilité entre paramètres, qui s’ajoute à H et limite les configurations admissibles. C’est ce processus (réduire, ajouter, re-trier) qui fait converger la chaîne vers une « triangulation » réellement équivalente au système, et c’est lui que la cellule suivante implémente.
def main_var(f, varlist):
'''Variable principale : la plus grande variable (ordre d'elimination) qui apparait.'''
for v in reversed(varlist):
if Poly(f, v).degree() > 0:
return v
return None # polynome dans les seuls coefficients
def rank_p(p_, varlist):
'''(indice de la variable principale, degre en celle-ci) -- ordre lexicographique.'''
mv = main_var(p_, varlist)
return (varlist.index(mv), Poly(p_, mv).degree()) if mv else (-1, 0)
for f, vl, attendu in [(h1, V1, "xm"), (h2, V1, "ym"), (g1, V1, "xm ou moins")]:
mv = main_var(expand(f), vl)
print(f"mv({str(expand(f))[:30]:30s}) = {mv} rang = {rank_p(expand(f), vl)}")mv(-u1 + 2*xm ) = xm rang = (2, 1)
mv(-u2 + 2*ym ) = ym rang = (3, 1)
mv(-u1**2 + 2*u1*xm ) = xm rang = (2, 1)def basic_set(H, varlist):
'''Selection gloutonne (Chou) : un polynome par variable principale, par rang croissant.'''
B, used = [], set()
for p_ in sorted(H, key=lambda q: rank_p(q, varlist)):
mv = main_var(p_, varlist)
if mv is None:
return [p_] # polynome sans variable : contrainte isolee, casse la chaine
if mv not in used:
B.append(p_)
used.add(mv)
return B
print("basic_set([h1, h2]) ->", [str(b) for b in basic_set(H1, V1)])basic_set([h1, h2]) -> ['-u1 + 2*xm', '-u2 + 2*ym']def char_set_basic(H, varlist, max_iter=80):
'''Iteration de Chou : basic-set + pseudo-reduction des non-retenus jusqu'a stabilite.
Retourne (chaine, nombre d'iterations). En cas de non-convergence en max_iter
iterations, echec explicite (RuntimeError).
'''
H = [expand(h) for h in H]
for it in range(max_iter):
B = basic_set(H, varlist)
R = []
for h in H:
if h in B:
continue
r = h
for p_ in reversed(B): # reduire depuis le sommet de la chaine
mv = main_var(p_, varlist)
r = prem_s(r, p_, mv) if mv else r
if r != 0:
R.append(r) # reste non nul : H est enrichi
if not R:
return B, it # stabilite : la chaine porte H
H = sorted(set(H).union(R), key=lambda q: (rank_p(q, varlist), str(q)))
raise RuntimeError("pas de convergence de l'ensemble caracteristique")
B1, it1 = char_set_basic(H1, V1)
print(f"CS(T1) : {len(B1)} polynomes, converges en {it1} iterations")
for b in B1:
print(f" {b} (var principale : {main_var(b, V1)})")CS(T1) : 2 polynomes, converges en 0 iterations
-u1 + 2*xm (var principale : xm)
-u2 + 2*ym (var principale : ym)Pour T1, la chaîne est exactement le système initial — deux équations triangulaires propres, l’une en \(x_m\), l’autre en \(y_m\). C’est le cas idéal ; les itérations de Chou ne servent que lorsque les hypothèses se contraintent mutuellement.
5. Le test de Wu
Le test : calculer le pseudo-reste de la conclusion successivement à travers la chaîne, depuis le polynôme de plus grande variable (le sommet) vers la base :
\[R = \operatorname{prem}\big(\dots \operatorname{prem}(\operatorname{prem}(g, f_r, mv_r), f_{r-1}, mv_{r-1}) \dots, f_1, mv_1\big)\]
Le critère : si \(R \equiv 0\), le théorème est prouvé — modulo les initiales (voir §6). L’intuition : la chaîne étant triangulaire, pseudo-diviser par le sommet élimine la plus grande variable, puis l’étage suivant élimine la suivante ; si tout s’annule, g est forcé à zéro par les équations de la chaîne, exactement comme une substitution montante l’établirait — mais sans jamais devoir résoudre les équations (aucune racine carrée, aucun dénominateur : tout reste polynomial).
L’idée de la preuve du critère (trois lignes). Sur la composante du lieu des zéros où les initiales ne s’annulent pas, chaque équation \(f_i = 0\) de la chaîne se résout (de façon qualitative) en sa variable principale \(v_i\) : \(v_i\) est « déterminé » par les variables plus petites. La pseudo-division par le sommet \(f_r\) remplace g par un polynôme de degré plus petit en \(v_r\) ; tant que ce degré est \(\geq\) le degré de \(f_r\), l’équation \(f_r = 0\) permet de continuer à réduire… jusqu’à obtenir R indépendant de \(v_r\). On recommence avec \(f_{r-1}\), etc. Le théorème de Ritt-Wu dit exactement cela : \(\operatorname{prem}(g, \text{CS}) = 0\) sur un domaine non dégénéré \(\implies g\) s’annule partout sur ce domaine dès que les hypothèses s’y annulent.
flowchart LR
A[Theoreme geometrique] --> B[Choix de repere<br/>parametres vs inconnues]
B --> C[Hypotheses polynomiales H<br/>conclusion g]
C --> D[char_set_basic :<br/>triangulation par pseudo-reste]
D --> E[prem successifs de g<br/>a travers la chaine]
E --> F{Reste identiquement nul ?}
F -->|oui| G[PROUVE modulo initiales<br/>non-degenerescences auto]
F -->|non| H[Encodage faux ?<br/>conditions cachees ?<br/>accretion 03b : Ritt]
G --> I{Verification croisee<br/>Groebner sature Rabinowitsch}
I -->|accord| J[Theoreme valide]
I -->|desaccord| K[Revenir a l'encodage]Le diagramme est le squelette du notebook : chaque nœud correspond à une cellule ; les nœuds F et I sont les deux portes où l’on refait le tour de l’encodage — précisément ce que le notebook éprouve au §9 (énoncé faux) ; le cas dégénéré, lui, est l’objet de l’accrétion Geometry-03b.
Trace sur T1 : la chaîne est [h₁: 2x_m − u₁, h₂: 2y_m − u₂]. Le sommet h₂ a y_m pour variable principale : prem(g1, h₂, y_m) tue les termes en y_m — ici g₁ ne dépend pas de y_m (les y s’annulent dans MA² − MB²), le reste est g₁ tel quel — puis on divise par h₁ en x_m : r = lc·g₁ − cr·x_m·h₁ avec cr = coefficient en x_m de g₁ = 2u₁·… — le calcul est laissé à la machine, la cellule ne met que 3 millisecondes. Le zéro final est exact : scripté au polynôme près, pas une approximation.
def wu_prem(g, B, varlist):
'''Pseudo-reste successif de g a travers la chaine B, du sommet vers la base.'''
R = expand(g)
for p_ in reversed(B):
mv = main_var(p_, varlist)
R = prem_s(R, p_, mv) if mv else R
return R
t0 = time.time()
R1 = wu_prem(g1, B1, V1)
print(f"prem(g, CS) = {R1} [{time.time()-t0:.3f}s]")
print("VERDICT :", "PROUVE" if R1 == 0 else "NON NUL")prem(g, CS) = 0 [0.004s]
VERDICT : PROUVELecture du résultat (T1)
L’élimination a fait tout le travail : le pseudo-reste par le sommet de la chaîne (h₂, en y_m) tue les termes en y_m (g₁ n’en contenait déjà pas après l’annulation des y²), puis l’étage h₁ (en x_m) élimine x_m au prix de l’identité \(2 \cdot g_1 = q \cdot h_1 + 0\) — le facteur 2 = initiale de h₁, inoffensif ici car constant. Pour un théorème de « collège », la preuve complète tient en deux divisions polynomiales.
Deux enseignements généraux à retenir dès ce premier succès : (1) le test ne « voit » pas la géométrie — il n’a manipulé que des polynômes, et le résultat zéro est un fait algébrique pur, reproductible sur n’importe quelle machine avec n’importe quel moteur (c’est la définition d’une preuve calculatoire) ; (2) la difficulté d’un théorème pour la méthode ne se mesure pas à sa difficulté humaine : ce qui compte, c’est la forme algébrique après encodage — d’où l’importance cruciale du choix des coordonnées au §2, le seul endroit où l’intelligence humaine reste indispensable.
T1 est prouvé en quelques millisecondes, par pure élimination polynomiale — sans avoir résolu le moindre système.
6. Les conditions de non-dégénérescence : les initiales
La contrepartie du critère : la pseudo-division multiplie par les coefficients dominants de la chaîne. Le raisonnement n’est valide que là où ces coefficients dominants — les initiales — ne s’annulent pas. Ce sont les conditions de non-dégénérescence du théorème, et la méthode les produit automatiquement : chacun des initiaux non constants est une hypothèse supplémentaire qu’il faut supposer vraie.
C’est une clef de lecture géométrique précieuse : un initial qui s’annule signale en général une configuration dégénérée (points confondus, droites parallèles qui devaient se couper, dénominateur nul d’un rapport…). L’article de référence souligne que cette génération automatique de non-dégénérescences est l’un des atouts de la méthode face aux approches par LLM, qui les ignorent souvent — et « prouvent » ainsi des énoncés faux dans les cas limites.
Règle de lecture d’un initial : il est le coefficient du terme de plus haut degré en la variable principale de son polynôme de chaîne. Pour T3 par exemple, la cellule du §8 montrera l’initiale \(q\,(t_1 t_2 - t_1 - t_2)\) — dont l’annulation s’écrit aussi \(q(t_1 + t_2 - t_1 t_2) = 0\), et c’est exactement la condition « (AD) ∥ (BE) » : les deux droites dont on cherche l’intersection O deviennent parallèles, O n’existe plus à distance finie, et le théorème de Ceva au sens usuel (concurrence) n’a pas de sens — l’initiale est alors \(q = 0\) (triangle aplati) ou la relation de parallélisme (vérifiable en deux lignes de déterminant). Ce que l’algorithme « voit » comme une division illicite, le géomètre le lit comme un cas limite de la figure : c’est le même objet, découvert automatiquement.
La convention de « preuve » : dans la littérature (Chou), un théorème est déclaré prouvé par Wu sans conditions si toutes ses initiales sont des constantes ; génériquement prouvé si les conditions nécessaires sont génériquement satisfaites ; sinon l’énoncé doit être amendé. Une preuve avec initiale non constante n’est pas fausse — elle est hypothétique, et c’est cette honnêteté-là (nulle part magique) que les systèmes à base de LLM réintègrent aujourd’hui.
def initials(B, varlist):
'''Initiales de la chaine : coefficients dominants en la variable principale.'''
out = []
for b in B:
mv = main_var(b, varlist)
if mv is not None:
out.append(Poly(b, mv).LC())
return out
init1 = initials(B1, V1)
print("Initiales de CS(T1) :", init1)
print("Verdict : tous constants ->", "AUCUNE condition : T1 est inconditionnel" if all(i.is_number for i in init1) else "conditions a interpreter")Initiales de CS(T1) : [2, 2]
Verdict : tous constants -> AUCUNE condition : T1 est inconditionnelPour T1, les initiales valent 2 : le théorème est prouvé sans aucune hypothèse parasite — il est inconditionnel (y compris dans les cas dégénérés u₁ = 0 ou u₂ = 0, que l’énoncé classique exclut mais que le résultat polynomial couvre quand même).
7. Vérification indépendante : bases de Gröbner saturées
Une preuve mérite un second moteur. Le critère de l’appartenance au radical se vérifie par Gröbner via l’astuce de Rabinowitsch : g s’annule sur V(H) privé de V(J) si et seulement si
\[\langle H,\; z\cdot J - 1,\; w \cdot g - 1 \rangle = \langle 1 \rangle\]
où J est le produit des non-dégénérescences à préserver et z, w des variables fraîches. L’intuition : z·J − 1 force J ≠ 0 (J inversible — l’adjonction d’une équation z·J = 1 inverse J, d’où le nom), w·g − 1 force g ≠ 0 ; si le tout a un zéro commun, c’est un point où H s’annule, J ≠ 0, g ≠ 0 — un contre-exemple. Si la base de Gröbner se réduit à ⟨1⟩, aucun tel point n’existe : g s’annule identiquement là où H = 0 et J ≠ 0. (Sans l’inverse de g, on ne parle que d’appartenance à l’idéal radical — la saturation par Rabinowitsch est ce qui transforme la « dureté » de l’idéal en un test de zéro de polynôme pur.)
Pourquoi exiger un second moteur : la méthode de Wu et le test de Gröbner partagent la même source de vérité mathématique mais zéro ligne de calcul commune — l’un élimine étage par étage, l’autre réécrit l’idéal entier sous ordre lexicographique. Deux organes indépendants qui se recoupent sur chaque théorème du notebook, c’est le croisement minimal de la méthode scientifique : l’accord ne prouve pas l’absence d’erreur dans l’encodage, mais un désaccord aurait forcé à le soupçonner. (Pour mémoire : c’est la vérification numérique du §8 — la première ligne de défense, moins chère que n’importe quel moteur — qui a réellement attrapé l’erreur de rapport dirigé.)
def groebner_sat_verify(H, g, J, gens):
'''g s'annule sur V(H) hors V(J) ssi GB([H, z*J-1, w*g-1]) = [1] (Rabinowitsch).'''
z, w = symbols("_z _w")
eqs = list(H) + [z*J - 1, w*g - 1]
G = groebner(eqs, *(list(gens) + [z, w]), order="lex")
return len(G.polys) == 1 and G.polys[0].as_expr() == 1
t0 = time.time()
v1 = groebner_sat_verify(H1, g1, 1, V1) # J = 1 : aucune non-degenerescence
print(f"Groebner T1 : g in radical -> {v1} [{time.time()-t0:.2f}s]")
print("Deux moteurs independants (Wu, Groebner) concluent :", "ACCORD" if (R1 == 0) == v1 else "DESACCORD")Groebner T1 : g in radical -> True [0.00s]
Deux moteurs independants (Wu, Groebner) concluent : ACCORD8. Un théorème moins trivial : Ceva (T3)
T3 (Ceva). Soit ABC un triangle, D ∈ (BC), E ∈ (CA), F ∈ (AB) trois points sur les côtés (ou leurs prolongements). Les droites (AD), (BE), (CF) sont concourantes si et seulement si \(\dfrac{\overline{BD}}{\overline{DC}} \cdot \dfrac{\overline{CE}}{\overline{EA}} \cdot \dfrac{\overline{AF}}{\overline{FB}} = 1\) (rapports dirigés).
Encodage barycentrique. A = (0,0), B = (1,0), C = (p, q) — un paramètre de moins que le cas général, l’échelle étant libre. Les points des côtés par leurs paramètres :
| Point | Coordonnées | Paramètre |
|---|---|---|
| D | (1−t₁)B + t₁C = (1−t₁+t₁p, t₁q) | D = B + t₁·(C−B) |
| E | t₂C = (t₂p, t₂q) | E = A + t₂·(C−A) |
| F | (t₃, 0) | F = A + t₃·(B−A) |
O = (o₁, o₂) le point de concurrence — inconnue. Les trois hypothèses d’alignement sont des déterminants 2×2 nuls : O∈(AD), O∈(BE), O∈(CF).
⚠ Le piège des rapports dirigés. La conclusion de Ceva s’écrit avec CE/EA — le rapport au sommet C. Or E = A + t₂(C−A) donne \(\overline{CE}/\overline{EA} = \frac{1-t_2}{t_2}\), et non \(\frac{t_2}{1-t_2}\) : le paramétrage part de A, le rapport part de C. Encodé naïvement dans le mauvais sens, le « théorème » devient un énoncé faux — et toute la machinerie le rejettera bruyamment. (Erreur réellement commise puis détectée lors de la préparation de ce notebook : la vérification numérique du §suivant est le seul garde-fou fiable.) Après chasse aux dénominateurs, la conclusion correcte :
\[g_3 : t_1(1-t_2)\,t_3 - (1-t_1)\,t_2\,(1-t_3) = 0\]
Pourquoi trois paramètres t₁, t₂, t₃ indépendants ? C’est le cœur de l’encodage : le théorème de Ceva exprime la concurrence en fonction des trois positions des points D, E, F. Si on fixait t₃ = f(t₁, t₂) dans l’encodage des hypothèses, la conclusion serait « triviale par construction » — le théorème à prouver, lui, énonce précisément que la concurrence force cette relation. Le schéma d’encodage général de Wu : les hypothèses polynomiales laissent les paramètres dans ℚ(p₁,…,p_k, t₁, t₂, t₃), et la conclusion est une égalité polynomiale qu’il faut déduire — c’est le sens du « pseudo-reste = 0 ».
Règle d’hygiène du notebook : toujours le sanity check numérique avant le symbolique.
# Encodage de T3
p, q_, t1, t2, t3, o1, o2 = symbols("p q t1 t2 t3 o1 o2")
V3 = [p, q_, t1, t2, t3, o1, o2]
dx, dy = (1 - t1) + t1*p, t1*q_ # D
ex, ey = t2*p, t2*q_ # E
fx = t3 # F (fy = 0)
hAD = o1*dy - o2*dx # O, A, D alignes (determinant)
hBE = (o1 - 1)*ey - o2*(ex - 1) # O, B, E alignes
hCF = (o1 - p)*(-q_) - (o2 - q_)*(t3 - p) # O, C, F alignes (F_y = 0)
H3 = [expand(hAD), expand(hBE), expand(hCF)]
g3 = t1*(1 - t2)*t3 - (1 - t1)*t2*(1 - t3) # Ceva, rapports diriges corrects
print("H3 =", H3)
print("g3 =", g3)H3 = [o1*q*t1 - o2*p*t1 + o2*t1 - o2, o1*q*t2 - o2*p*t2 + o2 - q*t2, -o1*q + o2*p - o2*t3 + q*t3]
g3 = t1*t3*(1 - t2) - t2*(1 - t1)*(1 - t3)# Sanity numerique BIEN POSE : les hypotheses de Ceva sont la CONCURRENCE,
# on ne peut pas prendre t1, t2, t3 au hasard et esperer que (CF) passe par O.
# Protocole : triangle concret + t1, t2 donnes -> t3 DERIVE de la relation de Ceva
# -> la concurrence doit etre verifiee ; et un t3 hors relation doit la casser.
base = {p: 2, q_: 3, t1: Rational(3, 10), t2: Rational(2, 5)}
t3_ceva = solve(g3.subs(base), t3)[0]
print("t3 derive de Ceva :", t3_ceva)
for label, t3_val, attendu in [("t3 = Ceva", t3_ceva, 0), ("t3 quelconque (7/20)", Rational(7, 20), "non nul")]:
s = dict(base); s[t3] = t3_val
Osol = solve([hAD.subs(s), hBE.subs(s)], [o1, o2], dict=True)[0]
s.update(Osol)
print(f"{label:22s} O = ({s[o1]}, {s[o2]}) hCF(O) = {hCF.subs(s)} [{attendu}]")t3 derive de Ceva : 14/23
t3 = Ceva O = (26/29, 18/29) hCF(O) = 0 [0]
t3 quelconque (7/20) O = (26/29, 18/29) hCF(O) = -357/580 [non nul]# CS + test de Wu sur T3
t0 = time.time()
B3, it3 = char_set_basic(H3, V3)
t_cs = time.time() - t0
t0 = time.time()
R3 = wu_prem(g3, B3, V3)
t_test = time.time() - t0
print(f"CS(T3) : {len(B3)} polynomes (convergence en {it3} iterations, {t_cs:.2f}s)")
for b in B3:
print(f" mv={main_var(b, V3)} deg={Poly(b, main_var(b, V3)).degree()} {str(b)[:70]}...")
print(f"prem(g3, CS) = {R3} [{t_test:.2f}s]")
print("VERDICT :", "PROUVE" if R3 == 0 else "NON NUL")CS(T3) : 3 polynomes (convergence en 2 iterations, 0.16s)
mv=t3 deg=1 -2*p*q**2*t1**2*t2*t3 + p*q**2*t1**2*t2 + p*q**2*t1**2*t3 + p*q**2*t1*...
mv=o1 deg=1 o1*q*t1*t2 - o1*q*t1 - o1*q*t2 + p*q*t1*t2 - q*t1*t2 + q*t2...
mv=o2 deg=1 -o1*q + o2*p - o2*t3 + q*t3...
prem(g3, CS) = 0 [0.01s]
VERDICT : PROUVELecture du résultat (T3)
La chaîne de T3 est plus riche que celle de T1 : trois polynômes (donc trois variables principales — les inconnues o₁, o₂ et un paramètre émergent), contre deux pour T1. C’est l’empreinte d’un énoncé à paramètres : l’itération de Chou a réduit deux à deux les occurrences redondantes (les trois alignements partagent les inconnues o₁, o₂) jusqu’à obtenir une triangulation où chaque équation détermine sa variable.
Le test a mis une fraction de seconde — 0,1 s typiquement — là où une base de Gröbner complète du même système demande déjà davantage : c’est l’élimination incrémentale qui paie. Et le reste est exactement zéro : pas une simplification approchée, un polynôme identiquement nul. Le théorème de Ceva est prouvé — la cellule suivante dit sous quelles conditions.
# Non-degenerescences auto-generees par la preuve : les initiales de CS(T3)
init3 = initials(B3, V3)
J3 = 1
for i in init3:
if not i.is_number:
J3 = expand(J3 * i)
print("Initiales non constantes :")
for i in init3:
if not i.is_number:
print(" -", str(i)[:90])
print("\nUne lecture geometrique possible : ces conditions excluent les triangles aplatis (q = 0),")
print("les sommets degeneres et les points D, E, F confondus avec un sommet -- exactement les cas")
print("ou l'enonce parle de droites mal definies ou de rapports 0/0.")Initiales non constantes :
- -2*p*q**2*t1**2*t2 + p*q**2*t1**2 + p*q**2*t1*t2 + 2*q**2*t1**2*t2 - q**2*t1**2 - 3*q**2*t
- q*t1*t2 - q*t1 - q*t2
- p - t3
Une lecture geometrique possible : ces conditions excluent les triangles aplatis (q = 0),
les sommets degeneres et les points D, E, F confondus avec un sommet -- exactement les cas
ou l'enonce parle de droites mal definies ou de rapports 0/0.# Verification Groebner saturee de T3, AVEC la non-degenerescence J3 produite par Wu.
# C'est la boucle complete : Wu prouve ET produit ses conditions ; Groebner certifie
# le meme enonce sous les memes conditions -- sans partager une ligne de code avec Wu.
t0 = time.time()
v3 = groebner_sat_verify(H3, g3, J3, V3)
print(f"Groebner sature T3 (J = produit des initiales) -> {v3} [{time.time()-t0:.1f}s]")Groebner sature T3 (J = produit des initiales) -> True [0.0s]9. Témoin négatif : la méthode doit aussi savoir dire non
Un outil de preuve qui n’échoue jamais sur un énoncé faux ne prouve rien. Test de résistance : gardons les hypothèses de T1 mais remplaçons la conclusion par un énoncé faux — « MA² = 4·MB² » (vrai seulement pour des triangles très particuliers, pas en général). Le test de Wu doit rendre un reste non nul, et la base de Gröbner saturée doit confirmer que le polynôme ne s’annule pas identiquement sur la variété des hypothèses.
Pourquoi le témoin négatif est un test de méthode, pas de gadget : les moteurs de preuve symboliques ne connaissent que des cas d’école positifs dans les démonstrations publiées — personne ne publie les énoncés faux qu’il a fallu rejeter pour stabiliser un encodage. Le comportement attendu du test de Wu sur un énoncé faux est clair, lui : la chaîne n’implique pas g, le dernier reste non nul survit, et le théorème n’est pas « prouvé ». C’est exactement la dissymétrie saine entre un outil de recherche (qui propose) et un outil de preuve (qui exige d’être mis en échec pour être cru) — et c’est précisément le registre dans lequel les LLM géométriques échouent encore : ils ne « proposent » pas une construction en la déclarant prouvée par le raisonnement symbolique qui la vérifie.
g1_faux = (xm**2 + ym**2) - 4*((xm - u1)**2 + ym**2) # MA^2 - 4 MB^2 : faux en general
R1f = wu_prem(g1_faux, B1, V1)
print("prem(g_faux, CS) =", R1f)
print("VERDICT :", "REJETE (reste non nul)" if R1f != 0 else "prouve ?!")
v1f = groebner_sat_verify(H1, g1_faux, 1, V1)
print("Groebner confirme : g_faux dans le radical ->", v1f, "(False = bien un contre-exemple general)")
cfg = {u1: 4, u2: 3, xm: Rational(2), ym: Rational(3, 2)}
print("Temoir concret u1=4 : g_faux(cfg) =", g1_faux.subs(cfg), "!= 0")prem(g_faux, CS) = -12*u1**2 - 12*u2**2
VERDICT : REJETE (reste non nul)
Groebner confirme : g_faux dans le radical -> False (False = bien un contre-exemple general)
Temoir concret u1=4 : g_faux(cfg) = -75/4 != 010. Exercices
Exercice 1 — Le parallélogramme. Encoder et prouver : « les diagonales d’un parallélogramme ABCD se coupent en leur milieu ». Repère suggéré : A = (0,0), B = (u₁, 0), D = (u₂, u₃) — C en est l’inconnue. Étapes : (1) traduire « ABCD parallélogramme » en une équation sur C (deux équations, une par composante : C = B + D − A) ; (2) écrire la conclusion : les milieux des diagonales [AC] et [BD] coïncident — deux égalités de coordonnées, quatre équations d’écart à annuler ; (3)
char_set_basic+wu_prem; (4) vérifier pargroebner_sat_verify(J = 1?). Indices : les hypothèses sont deux équations en x_c, y_c — la chaîne sera déjà triangulaire ; le sanity numérique (u₁, u₂, u₃ concrets) doit passer avant le symbolique, comme dans tout ce notebook.
Exercice 2 — Le centre de gravité. Encoder : « les trois médianes d’un triangle sont concourantes, et le point de concurrence divise chaque médiane dans le rapport 2:1 ». S’inspirer de l’encodage de Ceva (T3) : D milieu de [BC], E milieu de [CA], F milieu de [AB] (trois égalités de moyennes = hypothèses affines avec paramètres du milieu — ici t₁ = t₂ = t₃ = 1/2, on peut les spécialiser directement…) ; les hypothèses de concurrence : O ∈ (AD), O ∈ (BE) ; la conclusion : O ∈ (CF) et le rapport, par exemple \(\overrightarrow{AO} = \frac{2}{3}\overrightarrow{AD}\) (deux équations). Attention aux rapports dirigés — le piège du §8. Indices : écrire O = A + λ(D − A) introduit λ en variable auxiliaire ; vérifier avec un triangle numérique avant la preuve symbolique.
# Exercice 1 -- le parallelogramme : a completer
# Etape 1 : variables et points (A=(0,0), B=(u1,0), D=(u2,u3) parametres ; C inconnue)
# TODO etudiant
resultat_ex1 = None # a remplacer par prem(g, CS) une fois la preuve lancee
print("Exercice a completer")Exercice a completer# Exercice 2 -- le centre de gravite : a completer
# Etape 1 : reprendre l'encodage de T3 ; les medianes passent par les milieux des cotes
# Etape 2 : deux alignements (medianes issues de A et B) comme hypotheses, O inconnue
# Etape 3 : conclure sur la troisieme mediane et le rapport dirige 2:1
# TODO etudiant
resultat_ex2 = None
print("Exercice a completer")Exercice a completerConclusion
Ce notebook a construit, à partir de zéro, le cœur de la méthode de Wu :
| Brique | Rôle | Où |
|---|---|---|
prem_s |
pseudo-division sans fraction — l’atome de l’élimination | §3 (confronté à sympy.prem) |
char_set_basic |
chaîne ascendante par itération de Chou — la triangularisation | §4 |
wu_prem |
test : la conclusion réduite par la chaîne | §5 |
initials |
non-dégénérescences auto-générées par la preuve | §6, §8 |
groebner_sat_verify |
second moteur indépendant (Rabinowitsch) | §7 |
Vérifions la cohérence globale des critères — les trois comportements attendus d’un système de preuve sain sont : (1) un énoncé vrai et inconditionnel est prouvé par Wu et par Gröbner (T1), sans aucune condition ajoutée ; (2) un énoncé vrai mais à conditions cachées est prouvé par Wu avec des initiales non constantes, et Gröbner confirme la même vérité sous la même hypothèse J ≠ 0 (T3) ; (3) un énoncé faux est rejeté par les deux (témoin négatif du §9). Un quatrième comportement existe — un énoncé vrai dont la version polynomiale échoue sur des composantes dégénérées, où le test devient non-concluant à raison — mais il excède le propos de ce notebook : il est traité par l’accrétion Geometry-03b. Le sanity check numérique reste, lui, en amont de tous les moteurs : encodage correct = préalable, pas conséquence.
Le bilan expérimental : deux théorèmes prouvés en fractions de seconde (T1 inconditionnel, T3 avec non-dégénérescences explicites) et un énoncé faux proprement rejeté — trois comportements, chacun confirmé par deux moteurs indépendants.
La morale géométrique : traduire un énoncé en polynômes est délicat avant même d’invoquer un algorithme — rapports dirigés (le piège Ceva du §8), dénominateurs déblayés (la bombe à retardement que démonte l’accrétion Geometry-03b), configurations dégénérées. Le sanity check numérique systématique est le seul garde-fou peu coûteux. La morale algorithmique : l’élimination incrémentale (Wu) est dramatiquement moins chère que la réécriture globale (Gröbner) sur les problèmes géométriques — et c’est elle que les systèmes neuro-symboliques SOTA réintègrent aujourd’hui comme moteur de preuve exact.
Au-delà de ce notebook : la décomposition de Ritt n’est pas implémentée ici — elle est l’objet de l’accrétion Geometry-03b ; les bases de Gröbner saturées du §7, elles, deviennent vite coûteuses — c’est assumé : le propos était de montrer pourquoi l’élimination incrémentale de Wu est le bon moteur d’abord. Enfin, la pédagogie de la série : chaque énoncé prouvé ici doit passer par les trois portes (sanity numérique, test de Wu, Gröbner croisé) — les refaire sur vos propres encodages est le meilleur entraînement aux pièges de la traduction géométrie → polynômes.
Pour aller plus loin
- Sinha et al. 2024 (arXiv:2404.06405) — l’étude IMO-AG-30 : Wu seul 15/30 ; Wu couplé aux méthodes synthétiques DD+AR (deductive databases, angle, ratio and distance chasing) 21/30, niveau argent ; Wu+AlphaGeometry 27/30, au-dessus du niveau or. Deux problèmes ne sont résolus que par Wu.
- Chou, Mechanical Geometry Theorem Proving (1988) — des centaines de théorèmes traités, le recueil de référence des encodages.
- Wu 1978 — l’article fondateur ; Ritt 1950 — la théorie des ensembles caractéristiques.
- Dans ce dépôt : la série SMT/Z3 (décision sous contraintes), la série Lean (preuve vérifiée par noyau) — deux autres réponses à « comment faire vérifier un raisonnement par une machine ».
Notebook de la série Geometry — SymbolicAI. Fait partie du cycle complet du raisonnement vérifiable du dépôt CoursIA.