Consider the following attempt at a ``thought-free'' proof of Morley's
Theorem.


Let $(x\_1,y\_1)$, $(x\_2,y\_2)$ and $(x\_3,y\_3)$ denote three vertices of
a generic triangle.


Let $(a\_1,b\_1)$, $(a\_2,b\_2)$ and $(a\_3,b\_3)$ denote three more points
in the plane.


For all $\lbrace i,j,k\rbrace=\lbrace 1,2,3\rbrace$, we want to impose the condition that
the line determined by $(x\_i,y\_i)$ and $(a\_k,b\_k)$ bisects the angle
from $(a\_j,b\_j)$ to $(x\_i,y\_i)$ to $(x\_j,y\_j)$. Capturing this
algebraically amounts to equating two squared cosines:
$$ \frac{((x\_i-a\_k)(x\_i-a\_j)+(y\_i-b\_k)(y\_i-b\_j))^2}
 {((x\_i-a\_k)^2+(y\_i-b\_k)^2)((x\_i-a\_j)^2+(y\_i-b\_j)^2)}$$
$$ = \frac{((x\_i-a\_k)(x\_i-x\_j)+(y\_i-b\_k)(y\_i-x\_j))^2}
 {((x\_i-a\_k)^2+(y\_i-b\_k)^2)((x\_i-x\_j)^2+(y\_i-x\_j)^2)}
$$
which simplifies first to
$$
((x\_i-a\_k)(x\_i-a\_j)+(y\_i-b\_k)(y\_i-b\_j))^2((x\_i-x\_j)^2+(y\_i-x\_j)^2)$$
$$ -
((x\_i-a\_k)(x\_i-x\_j)+(y\_i-b\_k)(y\_i-x\_j))^2((x\_i-a\_j)^2+(y\_i-b\_j)^2)=0.
$$
Then expanding the left side and dividing out by the condition
$$ -a\_jy\_i - b\_jx\_j + x\_ib\_j - x\_ix\_j + y\_ix\_j + a\_jx\_j$$
(of having $(a\_j,b\_j)$,$(x\_i,y\_i)$ and $(x\_j,y\_j)$ collinear) leaves
$$C\_{ijk}:=a\_jy\_i^3-x\_i^3b\_j+2x\_ix\_jy\_ib\_j-2x\_ia\_jy\_ix\_j-2a\_ky\_i^3+2x\_i^3b\_k+b\_k^2x\_ix\_j+y\_i^3x\_j-x\_i^3x\_j$$
$$-a\_k^2y\_ix\_j+2a\_kx\_ib\_kx\_j-2a\_kx\_jb\_ky\_i-2a\_kb\_kb\_jy\_i+2x\_ja\_kb\_kb\_j+2x\_jb\_ky\_ib\_j-2x\_ja\_ky\_ib\_j$$
$$-2x\_jx\_ib\_kb\_j+2a\_ky\_i^2b\_j-a\_k^2x\_ib\_j+2a\_kx\_i^2b\_j+b\_k^2x\_ib\_j-2b\_k^2y\_ix\_i+2a\_k^2x\_iy\_i+x\_ja\_k^2b\_j$$
$$-x\_jb\_k^2b\_j-a\_jx\_jb\_k^2+a\_jx\_ja\_k^2-a\_ja\_k^2y\_i+a\_jb\_k^2y\_i-2a\_jb\_kx\_i^2-2a\_jb\_ky\_i^2-2x\_ja\_kx\_ib\_j$$
$$+2a\_jx\_ja\_ky\_i-2a\_jx\_ja\_kb\_k-2a\_jx\_ja\_kx\_i+2a\_jx\_jb\_ky\_i+2a\_jx\_ib\_kx\_j+2a\_ja\_kx\_ib\_k+2a\_kx\_jy\_i^2$$
$$-2y\_i^2b\_kx\_j+b\_k^2y\_ix\_j+2x\_i^2a\_kx\_j+x\_i^2y\_ix\_j-2x\_i^2b\_kx\_j-x\_ix\_jy\_i^2-a\_k^2x\_ix\_j+x\_i^2x\_ja\_j$$
$$-x\_jy\_i^2b\_j+a\_jy\_ix\_i^2-a\_jy\_i^2x\_j+x\_i^2b\_jx\_j-x\_ib\_jy\_i^2-2a\_kb\_kx\_i^2+2a\_kb\_ky\_i^2-2a\_ky\_ix\_i^2+2x\_ib\_ky\_i^2\ .$$


Now for Morley's theorem we would like to conclude that points
$(a\_1,b\_1)$, $(a\_2,b\_2)$ and $(a\_3,b\_3)$ form an equilateral triangle.
We can easily write down polynomials in $a\_1,b\_1,a\_2,b\_2,a\_3$ and
$b\_3$ all of whose vanishing would capture this. For example, it
would suffice to prove the vanishing of
$$I\_{123}:=-2a\_1a\_2+a\_2^2+2b\_1^2-2b\_1b\_2+b\_2^2+2a\_1a\_3-a\_3^2-2b\_1b\_3+b\_3^2\ .$$


Since we hope $I\_{123}$ will vanish whenever
$C\_{123},C\_{213},C\_{312},C\_{132},C\_{231},C\_{321}$ do, we look to find
$I\_{123}$ in (the radical of) the ideal
$$C:=\langle C\_{123},C\_{213},C\_{312},C\_{132},C\_{231},C\_{321}\rangle.$$ Unfortunately, as
one can see from the above, all the generators of $C$ vanish if
$x\_1=y\_1=x\_2=y\_2=x\_3=y\_3=0$, and so the same must hold for every
element of $C$. Nevertheless $I\_{123}$ does not vanish on this
condition.


The classical nullstellensatz leaves only one way out: the vanishing
of $I\_{123}$ doesn't follow from the vanishing of all the $C\_{ijk}$
without the exploitation of some restriction on the range of the
variables such as confining them to the reals.


Question: What insight does the machinery of real algebraic geometry
shed on the shape of a proof of Morley's Theorem along the lines of
this sketch?



Morley's Theorem and real algebraic geometry
This isn't a matter of real versus complex geometry -- the equations you give aren't enough to encode Morley's theorem over the reals. Let $z\_1 z\_2 z\_3$ be our original triangle; I will use indices that are cyclic modulo $3$. Let $\ell^0\_i$ be the trisector of the angle at $z\_i$ which is closer to $z\_{i-1}$ and let $m^0\_i$ be the trisector which is closer to $z\_i$. Let $\ell^1\_i$ and $\ell^2\_i$ be the rotations of $\ell^0\_i$ by $120^{\circ}$ and $240^{\circ}$, and define $m^1\_i$ and $m^2\_i$ likewise.


For $r=1$, $2$ and $3$, let $(\delta\_r, \epsilon\_r)$ equal to one of $(0,0)$, $(1,2)$ or $(2,1)$. Let $c\_r$ be the intersection of $m^{\epsilon\_r}\_r$ and $\ell^{\delta\_{r+1}}\_{r+1}$. Then $\angle z\_r z\_{r+1} c\_r = \angle c\_r z\_{r+1} c\_{r+1} = \angle c\_{r+1} z\_{r+1} z\_{r+2}$ so your equations hold for $(x\_r, y\_r) = z\_r$ and $(a\_r, b\_r) = c\_r$. 


Of the $81$ possible choices for $(\delta\_r, \epsilon\_r)$, I believe that the triangle $c\_1 c\_2 c\_3$ is equilateral only for $54$ of them. I am basing this on [Connes' proof](http://www.alainconnes.org/docs/morley.pdf) of Morley's theorem, where a key hypothesis is that 
$$\sum\_{r=1}^3 \angle c\_{r-1} z\_{r} c\_{r} = \pm 60^{\circ} \ \mbox{not} \ 180^{\circ}.$$
Connes' rotation $g\_r$ is a rotation around $z\_r$ by angle $2 \angle c\_{r-1} z\_{r} c\_{r}$, so what he says is that $g\_1 g\_2 g\_3$ should be a nontrivial rotation.


It's easy enough to encode this condition algebraically. (If you have trouble with it I'll write more, but I bet you won't.) Once you do that, I think it should be easy to convert Connes proof into the sort of proof you are looking for. You'll also need to impose that certain things are nonzero, because Connes divides at times.


