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.

翻译：170多年来,施泰纳-莱曼斯定理学的一个直接证据表明,施泰纳-莱曼斯定理学一直未能达到几何参数,挑战在于,如果证据不依赖荒谬的推理,证据才被视为直接证据。因此,任何声称直接的证据都必须在回到正理时表明,所使用的所有辅助性定理也都得到了直接证明。在本文中,我们提供了斯坦纳-莱曼斯定理学的证明,保证该定理学是直接的。这一主张的证据来自我们的方法:我们为厄克利德恩平面的几何学正式确定了一个建设性的定理原理,作为执行建设性逻辑和根据这一建设性基础建立施泰纳-莱姆斯定理学证据的助理。