机械化应该是可行的. 已经取得的成果http://pub.ist.ac.at/~chl/ML2015/kragl-sma2015.pdf? Proof of Robbins conjecture using theorem proverEQP (1996)? Design and verification of Intel Core i7 processor using SAT technology (2009)? Certified Windows 7 device drivers using SMT (2010)? Flyspeck project: formal proof of the KeplerConjecture using Isabelle and HOL Light proof assistants (2014)我们可以额外添加删除公理, 证明或者反证某个问题. 限定公理体系, 可能存在不可判定问题.大多数理论专业不是因为聪明问题离开学术, 而且综合考虑经济因素离开. 只要努力做习题, 自然能学懂.可以考虑软件所或者自动化所, 从事计算复杂度, 机器学习, 模式识别等方向. 特别是计算复杂度, 跟机器证明完全不分家. Machine learning and automated theorem proving. James P. Bridge 用火红火红的deep learning to help the theorem prover?这样进退自如.目前, 感觉理论计算机方面的学者在主导这个领域(他们要做很多应用, 密码学, 软件可靠性验证), 因此代数几何方法好像并不Popular. 高小山他们用的代数几何方法, 确实很艰深.显著感觉国外CS界更关心这些, 因此推荐出国或者从事CS.http://staff.computing.dundee.ac.uk/katya/phd.html
■网友
简单地说这个想法一百年前希尔伯特就提出来了。即构造一个形式系统，它包含推理规则，可以自动进行推理。如此一来所有数学定理或问题都可以机械地求解。但哥德尔不完备定理粉碎了这个想法。
■网友
【数学机械化】 数学机械化是利用中国古代数学思维方式，再加上现代的计算机开展的一种研究数学方式。

■网友
题主现在的情况怎么样啊？我对这个方面也很感兴趣，能不能私信留个联系方式互相交流？

来源：(未知)

【】网址：/a/2020/0525/gd494207.html

标题：数学机械化