Steiner-Lehmus 定理的机器检验直接证明
计算机科学中的逻辑
2021-12-22 v1
摘要
Steiner-Lehmus 定理的直接证明已困扰几何学家逾 170 年。其难点在于，只有当证明不依赖于归谬法时才被视为直接证明。因此，任何声称直接的证明都必须回溯至公理，表明所用所有辅助定理亦为直接证明。本文给出了一则保证直接的 Steiner-Lehmus 定理证明。该主张的证据源于我们的方法：我们在实现构造性逻辑的 proof assistant 中形式化了欧氏平面几何的构造性公理集，并基于此构造性基础构建了 Steiner-Lehmus 定理的证明。
引用
@article{arxiv.2112.11182,
title = {A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem},
author = {Ariel Kellison},
journal= {arXiv preprint arXiv:2112.11182},
year = {2021}
}