Conway postulated that the Steiner-Lehmus theorem is unprovable using direct methods of proof. Can this be proven directly, that the Steiner-Lehmus theorem cannot be proven directly over Euclidean postulates?

I considered "porting" my question from the FOM mailing list to MathOverflow, as you have done, but decided against it because I now feel that it is not a well-posed question. If you want to ask this question then I would suggest rephrasing it as follows: "Is there a satisfactory way to define formally what a `direct proof' is?"
– Timothy ChowJul 6 '10 at 1:26

1

Note that the Conway article has a typo, the second form of the main equation should be $(c-a)\{ ac^2 + (a^2+3ab+b^2)c + b^2(a+b)\} = 0$.
– François G. Dorais♦Jul 6 '10 at 2:58

I doubt there is an answer better than Conway's answer: The proof must use some fact about the real numbers which is not true in an arbitrary field of characteristic zero. So coordinatize your proof and see what facts about the ground field are being used. For example, I believe that angle chasing, as in section 4.2 of Kiran Kedlaya's book math.mit.edu/~kedlaya/geometryunbound , works over any field.
– David SpeyerJul 6 '10 at 14:47

`$(c-a)\{ ac^2 + (a^2+3ab+b^2)c + b^2(a+b)\} = 0$`

. – François G. Dorais♦ Jul 6 '10 at 2:58