Part 5: Groebner (Grobner) basis and Wu Method: polynomial elimination methods

So far, in Parts 1-4, we have followed a mostly pure-math storyline: from Euclid's synthetic geometry, through analytic and algebraic viewpoints, all the way to the modern language of vectors, forms, and (eventually) geometric algebra - ideas that were already in very solid shape by the early 20th century. A natural next question is: what happened in roughly the last 50 years for solving Euclidean geometry problems? The next big step is algorithmic: turn geometry into a procedure. Translate points, lines, circles, and incidences into variables, and translate geometric constraints into polynomial equations. Once everything becomes polynomial, a proof turns into a computable elimination problem. In this part we introduce two seminal algebraic approaches to automated Euclidean theorem proving: Wu's method and the Groebner basis method.

Wu's method (Wen-Tsun / Wenjun Wu, late 1970s). Wu's method - often presented through characteristic sets (triangular-style elimination) - was developed by Wen-Tsun Wu in the late 1970s and became one of the first highly successful, systematic methods for mechanical theorem proving in elementary geometry [WU-ORIG] [WU-CHAR]. The key move is explicitly analytic: choose coordinates for "free" points, convert each geometric relation (collinearity, perpendicularity, equal lengths, parallelism, cyclicity, etc.) into polynomial constraints, then eliminate variables in a structured way until the target statement reduces to an algebraic consequence of the hypotheses [WU-CHAR]. Conceptually it's: geometry -> polynomials -> elimination, with a procedure that a computer can execute step-by-step.

Groebner basis method (Buchberger 1965; geometry automation later). Groebner bases were introduced by Bruno Buchberger (1965), together with the Buchberger algorithm, giving a general-purpose computational engine for polynomial ideal problems [GB-HIST] [GB-THESIS]. In geometry proving, the translation is clean: encode the hypotheses as an ideal I generated by polynomials, encode the desired conclusion as a polynomial g, and prove the theorem by checking whether g is in I (or in a saturation/elimination variant to handle degeneracies). Groebner bases make this membership test algorithmic via systematic reductions and elimination behavior [GB-HIST].

Same destination, different roads (and "coordinate dependence"). Both methods share the same punchline: a Euclidean proof can be reduced to algebraic elimination, once you choose coordinates and translate relations into polynomials [WU-CHAR] [GB-HIST]. This looks coordinate-dependent in execution because we literally pick a coordinate system, but the truth is coordinate-free: any non-degenerate coordinate choice represents the same geometry. Wu emphasized this as a workable philosophy of mechanization - geometry carries enough intrinsic structure that, after coordinatization, proof becomes a deterministic computation [WU-SURVEY]. That's the deeper shift of the last decades: not just knowing geometry, but compiling geometry into a procedure.

The rest of this part shows two classic algebraic geometry-prover styles on the same configuration:

1. Groebner basis method: prove the target polynomial lies in the ideal generated by hypothesis polynomials.
2. Wu's method style (characteristic-set / triangular elimination): eliminate variables using a triangular chain (here it becomes simple linear elimination).
3. Wu's method following the algorithm more faithfully to show the difference from (2).

We work entirely in polynomials (no square-roots) by proving the squared identity $$ (BE^2)(DH^2) - (BD^2)(EH^2) = 0, $$ which is equivalent to $BE\cdot DH = BD\cdot EH$ for positive lengths.

Notes on representation

• SymPy is used here for convenience (symbolic polynomials + Groebner/Wu-style elimination). It is not required in principle.
• Matrices are used only as a compact way to write determinants/dot products; this is a modeling choice, not a requirement of Wu's method.
• In a later program the geometry is built with Point objects in SymPy instead of matrices, to show a more geometric style; both approaches are equivalent.

5.1 Coordinate encoding of the geometry (bake-in the constraints)

Given:

• $AD \parallel BC$
• $\angle C = 90^\circ$
• $BC = CD$
• $E \in CD$, and $DE = AD$
• $EF \perp AB$
• $H = BD \cap EF$

We can choose coordinates (scale is irrelevant):

$$ C=(0,0),\quad B=(1,0),\quad D=(0,1) $$ so $BC\perp CD$ and $BC=CD=1$.

Since $AD\parallel BC$, line $AD$ is horizontal, so: $$ A=(a,1). $$

Point $E\in CD$ means $E=(0,e)$. Condition $DE=AD$ gives: $$ DE = 1-e,\quad AD = a \quad\Rightarrow\quad 1-e=a \Rightarrow e=1-a. $$ So: $$ E=(0,1-a). $$

Now let $H=(h_x,h_y)$ be the intersection point we will solve from the constraints:

• $B,D,H$ are collinear (because $H \in BD$)
• $(H-E)\perp(B-A)$ (because $H\in EF$ and $EF\perp AB$)

import sympy as sp
sp.init_printing()

def dist2(P, Q):
    v = P - Q
    return sp.expand(v.dot(v))

def sec(title):
    print("\n" + "="*70)
    print(title)
    print("="*70)

a, hx, hy = sp.symbols("a hx hy")

# Fixed points
C = sp.Matrix([0, 0])
B = sp.Matrix([1, 0])
D = sp.Matrix([0, 1])

# Variable point A, and derived point E
A = sp.Matrix([a, 1])
E = sp.Matrix([0, 1 - a])

# Variable point H
H = sp.Matrix([hx, hy])

Now we translate hypotheses into polynomials

Collinearity $B,D,H$

Vectors $\overrightarrow{DB} = B-D$ and $\overrightarrow{DH}=H-D$ must be linearly dependent, so the 2×2 determinant is zero: $$ \det\begin{pmatrix} B_x-D_x & B_y-D_y\\ H_x-D_x & H_y-D_y \end{pmatrix}=0. $$

Perpendicularity $(H-E)\perp(B-A)$

Dot product is zero: $$ (H-E)\cdot(B-A)=0. $$

These give two polynomials $f_1=0$, $f_2=0$.

sec("Hypothesis polynomials")

# (1) Collinear B, D, H
f1 = sp.Matrix([[B[0]-D[0], B[1]-D[1]],
                [H[0]-D[0], H[1]-D[1]]]).det()
f1 = sp.expand(f1)

# (2) (H-E) ⟂ (B-A)
f2 = sp.expand((H - E).dot(B - A))

print("f1 (collinear B,D,H) =", f1)
print("f2 ((H-E) ⟂ (B-A))  =", f2)

# For reference, simplify them:
print("\nSimplified forms:")
print("f1 =", sp.factor(f1))
print("f2 =", sp.factor(f2))

======================================================================
Hypothesis polynomials
======================================================================
f1 (collinear B,D,H) = hx + hy - 1
f2 ((H-E) ⟂ (B-A))  = -a*hx - a + hx - hy + 1

Simplified forms:
f1 = hx + hy - 1
f2 = -a*hx - a + hx - hy + 1

Target polynomial is the following identity to prove: $$ p := (BE^2)(DH^2) - (BD^2)(EH^2) = 0. $$

This is equivalent to $BE\cdot DH = BD\cdot EH$ because lengths are nonnegative.

sec("Target polynomial p")

BE2 = dist2(B, E)
BD2 = dist2(B, D)
DH2 = dist2(D, H)
EH2 = dist2(E, H)

p = sp.expand(BE2*DH2 - BD2*EH2)

print("BE^2 =", sp.factor(BE2))
print("BD^2 =", sp.factor(BD2))
print("DH^2 =", sp.factor(DH2))
print("EH^2 =", sp.factor(EH2))
print("\np = (BE^2)(DH^2) - (BD^2)(EH^2) =")
print(sp.sstr(sp.factor(p)))

======================================================================
Target polynomial p
======================================================================
BE^2 = a**2 - 2*a + 2
BD^2 = 2
DH^2 = hx**2 + hy**2 - 2*hy + 1
EH^2 = a**2 + 2*a*hy - 2*a + hx**2 + hy**2 - 2*hy + 1

p = (BE^2)(DH^2) - (BD^2)(EH^2) =
a*(a*hx**2 + a*hy**2 - 2*a*hy - a - 2*hx**2 - 2*hy**2 + 2)

5.2 Gröbner basis proof

We compute a Gröbner basis $G$ for the ideal $\langle f_1,f_2\rangle$.
Then reduce $p$ modulo $G$. If the remainder is 0, then $$ p \in \langle f_1,f_2\rangle $$ so the hypotheses imply the conclusion.

sec("| Groebner basis reduction")

G = sp.groebner([f1, f2], hx, hy, a, order="lex")

print("| Groebner basis polynomials:")
for g in G.polys:
    print("|   ", g.as_expr())

rem = G.reduce(p)[1]
print("\n| Remainder of p modulo Groebner basis =")
sp.pprint('| ' + sp.sstr(sp.factor(rem)))

assert rem == 0
print("\n| ✅ Groebner proof complete: remainder = 0")

======================================================================
| Groebner basis reduction
======================================================================
| Groebner basis polynomials:
|    hx + hy - 1
|    a*hy - 2*a - 2*hy + 2

| Remainder of p modulo Groebner basis =
| 0

| ✅ Groebner proof complete: remainder = 0

5.3 Wu’s method style proof (triangular elimination)

Wu’s method builds a triangular (ascending) chain and repeatedly takes pseudo-remainders to eliminate variables. Here, our constraints are already linear, so the “characteristic set” is essentially:

• from collinearity: $f_1= h_x + h_y - 1 = 0$
• from perpendicularity: $f_2= -a h_x - a + h_x - h_y + 1 = 0$ So elimination becomes:

1. From $f_1=0$:
   $$ h_y = 1-h_x. $$
2. Substitute into $f_2=0$ to solve $h_x$.
3. Substitute $(h_x,h_y)$ into $p$. If it becomes 0, the theorem is proved. This is exactly the same spirit as Wu: reduce the goal with the chain until remainder is 0. See the code below

sec("Wu-style triangular elimination")

# Step 1: solve f1 for hy
hy_expr = sp.solve(sp.Eq(f1, 0), hy)[0]
print("From f1=0, hy =", hy_expr)

# Step 2: substitute into f2 and solve for hx
f2_sub = sp.simplify(f2.subs(hy, hy_expr))
print("\nSubstitute hy into f2 ->")
sp.pprint(sp.factor(f2_sub))

hx_expr = sp.solve(sp.Eq(f2_sub, 0), hx)[0]
print("\nSolve for hx -> hx =", hx_expr)

# Then hy
hy_expr2 = sp.simplify(hy_expr.subs(hx, hx_expr))
print("And hy =", hy_expr2)

# Step 3: substitute into p
p_sub = sp.simplify(p.subs({hx: hx_expr, hy: hy_expr2}))
print("\nSubstitute (hx,hy) into p ->")
sp.pprint(sp.factor(p_sub))

assert sp.factor(p_sub) == 0
print("\n✅ Wu-style elimination complete: p reduces to 0")

======================================================================
Wu-style triangular elimination
======================================================================
From f1=0, hy = 1 - hx

Substitute hy into f2 ->
-a⋅hx - a + 2⋅hx

Solve for hx -> hx = -a/(a - 2)
And hy = 2*(a - 1)/(a - 2)

Substitute (hx,hy) into p ->
0

✅ Wu-style elimination complete: p reduces to 0

5.4 Extra: numeric sanity check

Since we are in python, we can pick any $a\in(0,1)$. (For the original picture you typically have $0<a<1$.)

We compute the actual numeric lengths and verify $BE\cdot DH = BD\cdot EH$.

sec("Numeric sanity check")

aval = sp.Rational(2, 5)   # a = 0.4
subs_num = {a: aval, hx: hx_expr.subs(a, aval), hy: hy_expr2.subs(a, aval)}

# Evaluate squared lengths
BE2_num = sp.N(BE2.subs(subs_num))
BD2_num = sp.N(BD2.subs(subs_num))
DH2_num = sp.N(DH2.subs(subs_num))
EH2_num = sp.N(EH2.subs(subs_num))

BE = float(sp.sqrt(BE2_num))
BD = float(sp.sqrt(BD2_num))
DH = float(sp.sqrt(DH2_num))
EH = float(sp.sqrt(EH2_num))

print("a =", float(aval))
print("H =", (float(subs_num[hx]), float(subs_num[hy])))
print("BE*DH =", BE*DH)
print("BD*EH =", BD*EH)
print("difference =", (BE*DH) - (BD*EH))

======================================================================
Numeric sanity check
======================================================================
a = 0.4
H = (0.25, 0.75)
BE*DH = 0.412310562561766
BD*EH = 0.412310562561766
difference = 0.0

This is Wu-flavored code, but it does not implement the full, original Wu characteristic-set algorithm.

In the real Wu method, you fix a variable order (a precedence like $h_y \succ h_x \succ \cdots$), then build a triangular chain (a characteristic set).

You do not "randomly solve" for a variable when it looks convenient. You pick eliminations to make the next polynomial's main variable well-behaved and the chain triangular.

Most importantly: Wu's method avoids fractions by using pseudo-division (a.k.a. pseudo-remainder). This guarantees you stay inside the polynomial ring: no denominators ever appear. Internally, pseudo-division multiplies by powers of the leading coefficient, so the working set always contains pure polynomials.

So we call it "Wu-style" elimination here: same spirit (triangular elimination), but the first version uses solve (which may introduce denominators), while the second version shows the truly programmable "no-denominator" elimination that resembles Wu's mechanics. Below we show how the problem would be solved if we followed Wu's algorithm more faithfully.

Fully programmable "no-denominator" Wu-like elimination (pseudo-remainder)

This is the key upgrade: we eliminate variables without ever dividing.

Core idea (one line)

To eliminate $h_y$, we replace "substitute $h_y=-b/a$" by pseudo-remainder:

$$R_2 = \operatorname{prem}(f_2, f_1; h_y),$$

which equals $a^k f_2(h_y=-b/a)$ but with denominators cleared, hence still a polynomial.

What this corresponds to mathematically

We built a triangular chain:

$$T_1 = f_1 \quad \text{(main variable } h_y),$$

$$T_2 = \operatorname{prem}(f_2, T_1; h_y) \quad \text{(main variable } h_x).$$

Then we reduced the goal:

$$p \xrightarrow{\operatorname{prem}(\cdot, T_1; h_y)} R_p \xrightarrow{\operatorname{prem}(\cdot, T_2; h_x)} 0.$$

That is exactly the "eliminate $h_y$, then eliminate $h_x$, then the goal collapses" story - but now in a Wu-programmable way.

One important Wu caveat (geometry degeneracy)

Pseudo-division implicitly assumes the leading coefficients used during elimination are not zero (otherwise the "main variable" disappears and you're in a degenerate case). In geometry, this corresponds to "generic position" assumptions (no coincident points, no accidental parallel collapse, etc.).

sec("Wu-style triangular elimination (pseudo-remainder / no-denominator)")

from sympy.polys.polytools import prem

# --- Step 1: eliminate hy using pseudo-remainder ---
T1 = sp.factor(f1)                         # main variable: hy
R2 = sp.factor(prem(f2, T1, hy))           # eliminates hy, stays polynomial

print("T1 (main var hy) =")
sp.pprint(T1)
print("\nR2 = prem(f2, T1, hy)  (hy eliminated, polynomial) =")
sp.pprint(R2)

# --- Step 2: eliminate hx using pseudo-remainder ---
T2 = sp.factor(R2)                         # main variable: hx (ideally)
Rp = sp.factor(prem(p, T1, hy))            # first reduce goal by T1 in hy
Rp2 = sp.factor(prem(Rp, T2, hx))          # then reduce by T2 in hx

print("\nT2 (after eliminating hy; main var should be hx) =")
sp.pprint(T2)
print("\nGoal reduction: Rp2 = prem(prem(p,T1,hy), T2, hx) =")
sp.pprint(Rp2)

assert sp.factor(Rp2) == 0
print("\n✅ Wu-style pseudo-remainder elimination: goal reduces to 0 (no denominators ever used)")

======================================================================
Wu-style triangular elimination (pseudo-remainder / no-denominator)
======================================================================
T1 (main var hy) =
hx + hy - 1

R2 = prem(f2, T1, hy)  (hy eliminated, polynomial) =
-a⋅hx - a + 2⋅hx

T2 (after eliminating hy; main var should be hx) =
-a⋅hx - a + 2⋅hx

Goal reduction: Rp2 = prem(prem(p,T1,hy), T2, hx) =
0

✅ Wu-style pseudo-remainder elimination: goal reduces to 0 (no denominators ever used)

References

• [ATP-GEO] Chou, Gao, Zhang (2001). "Machine Proofs in Geometry." Summary: Monograph on automated geometry theorem proving. URL: http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf
• [CAS-GEN] "Computer algebra systems: Mathematica, Maple." Summary: General-purpose CAS background for symbolic computation. URLs: https://en.wikipedia.org/wiki/Wolfram_Mathematica ; https://en.wikipedia.org/wiki/Maple_(software)
• [GB-HIST] Buchberger (2005). "An Introduction to Groebner Bases." Summary: Historical and conceptual introduction to Grobner bases. URL: https://www3.risc.jku.at/publications/download/risc_3045/2005-07-09-Historic-Intro-to-GB.pdf
• [GB-THESIS] Buchberger (1965/2005 translation). "Bruno Buchberger's PhD thesis (Grobner bases)." Summary: Original Grobner basis algorithm and theory; later English translation with commentary. URL: https://www.sciencedirect.com/science/article/pii/S0747717105001483
• [WU-CHAR] Wu (late 1970s). "Wu's method of characteristic set." Summary: Overview of characteristic-set elimination developed in the late 1970s. URL: https://en.wikipedia.org/wiki/Wu%27s_method_of_characteristic_set
• [WU-ORIG] Wu (late 1970s). "Wu's method discovery timeline." Summary: Historical timeline for the development of Wu's method. URL: http://www.mmrc.iss.ac.cn/~lzhi/Research/wuritt.html
• [WU-SURVEY] Wu et al. (2007). "Mathematics mechanization" survey. Summary: Survey of algebraic methods and mechanization in geometry proving. URL: http://www.mmrc.iss.ac.cn/~xgao/paper/07-mmsurvey.pdf