Resolution
Global GMS
ES Strata
Build. Blocks
Comb. Appl.
HCA Proving
Arrangements
Branches
Classify
Coding
Deformations
Equidim Part
Existence
Finite Groups
Flatness
Genus
Hilbert Series
Membership
Nonnormal Locus
Normalization
Primdec
Puiseux
Plane Curves
Saturation
Solving
Space Curves
Spectrum
Proof with Computer and Algebraic Geometry
We give a human-computer-aided  proof of the Theorem .
Here, we concentrate on case 1 (PSL(2,p)) -- cases 2 and 3 are similar, case 4 trivial, while case 5 is a bit more involved.
Construction: Fix the word  w = X-2 Y-1 X  and consider the matrices x , y in PSL(2,p):
x = | 0  -1 |                     y = | 1        b  |
| 1     t |                     | c   1+bc |
Note: U1 (x,y) = 1   has no solution over Fp .
The entries of   U1 (x,y) - U2 (x,y)   create a polynomial ideal   I   in   Z[b,c,t].
Statement: The theorem holds for PSL(2,p) <==> V(I) has a rational point in (Fp)3.
We show: V(I)   has rational points over   Fp  for all prime numbers p>3.
What is needed.

KL, 06/03 http://www.singular.uni-kl.de