有两种看待问题的方法，一种是从逻辑的角度来看，另一种是从心理学的角度来看。

要获得任何数学自动化的开始，您需要形式化您想要的部分。直到 20 世纪早期，大多数日常数学才被逻辑和集合论形式化。即使哥德尔的不完备性定理（非常松散地）说没有算法来决定数学陈述（包括算术理论）的定理，这仍然留下了很多可以决定的数学。但这需要逆向数学程序（仍在进行中）具体说明哪些数学子集是可判定的，或者在何种程度上（需要哪些逻辑假设）它们是不可判定的。

所以算术中的定理只有'+'（即删除'*'）可以确定，欧几里得几何 可以确定，单变量微积分可以确定，但不能确定单变量积分。这些例子表明，我们所知道的可判定是非常基本的。而且我们关心的大多数事情都是非常非基本的（几乎按照定义）。

至于心理学，你在数学课上学到的定理和证明与它们的形式化相去甚远。大多数数学家并没有像计算机那样在他们的脑海中推动符号。数学家更像是一位艺术家，将梦境形象化，并将隐喻与他们几乎没有意识的重复形象联系起来。也就是说，机器和数学家只是在不同的表示上工作（尽管非数学家可能会想象）。

为了解决您的具体问题，是的，数学定理和证明它们的系统在技术意义上非常相似。游戏（通常，并非总是）可以建模为树，同样，证明也可以建模为树。如果不给你写一个关于游戏和证明的书库，让我们说数学证明就像 Alpha Zero 赢得的游戏一样，不是为了特别有趣的定理。赢得一局围棋更像是证明一个非常非常大的布尔公式。大多数数学定理在其证明树中引入步骤时需要大量的独创性。事后检查证明是否正确可能是机械的，但发现证明几乎需要魔法才能在游戏中迈出一步。当然，数学中有些东西是可自动化（如前所述，导数），但某些数学系统（如积分）可证明不可能找到所有真实陈述的证明。

定理证明和游戏之间的另一个区别是，证明必须在所有路径上都是气密的，而在游戏中，一方只需勉强战胜另一方。

一个完全可能导致困难的单独问题是，我们可能还没有可用的工具，即编辑器、符号、证明助手，这些工具可以很容易地做应该很容易的事情。或者可能只是数学家不熟悉定理证明系统。

或者，如果有足够好的自动定理证明器，数学家就不会太在意它们，因为他们会带走自己寻找证明的乐趣。