  A direct proof of the Steiner-Lehmus theorem has eluded geometers for over
170 years. The challenge has been that a proof is only considered direct if it
does not rely on reductio ad absurdum. Thus, any proof that claims to be direct
must show, going back to the axioms, that all of the auxiliary theorems used
are also proved directly. In this paper, we give a proof of the Steiner-Lehmus
theorem that is guaranteed to be direct. The evidence for this claim is derived
from our methodology: we have formalized a constructive axiom set for Euclidean
plane geometry in a proof assistant that implements a constructive logic and
have built the proof of the Steiner-Lehmus theorem on this constructive
foundation.
