初等幾何に限定すれば定理の自動証明はある程度上手くいったりしないかな
補助線引いていくだけだったりするし