如何研发一个几何证明题的做题机器？

KeyTo9_Fans

我想开发一个程序，录入常用的几何证明推理规则，然后读入几何证明题的前提条件和需要证明的结论，然后采用迭代加深算法，先枚举1条推理规则，如果能推出结论，那么输出这条规则；否则枚举第1步和第2步的推理规则，如果能推出结论，那么输出第1步和第2步分别用的是哪条推理规则；否则枚举第1步、第2步和第3步的推理规则，如果能推出结论，那么输出这3步分别用的是哪条推理规则；依次类推，直到推出结论，或者用户没有耐心等待，手动终止程序为止。

我想问一下坛友们，我这个想法是否可行？如果不可行，实现它所遇到的最大的困难在哪里？

nyy

机械证明听过没？机器证明，用软件证明几何命题的，有专门的这个数学方向

282842712474

以前的严格思路是机械证明那一套，能保证正确性；现在的主流思路是ChatGPT那一套，有随机性，有错误的可能，但看起来创造力更强。

风云剑

吴文俊的“吴”方法？

楼主的方法是广度搜索，录入规则多的话，搜索树胖的厉害；录入规则少的话，搜索树瘦，但是很高。
chatGPT的话，大概可以算是有经验指导的深度搜索。