【总结】
这几天学了好多新的工具，而且网上教程少得可怜，java随便一个不知名的框架都比前三个工具的讲解详细哎。
Z3：比较专业的中文名叫做约束求解器，但确实挺厉害的，可以快速求出各种多元方程式的值，很好奇未来在研究方面应该如何施展。最大的优点是可以借助多门语言实现，python、java等待都可以，这点非常棒。
Coq：这是一种验证软件，但语法有些奇怪，目前只搞懂加减法这样的简单运算和教程里的一些验证方法。刚开始连执行语句都不会，教程本来就少，如何使用界面的教程就更少的可怜了，再加上那些憋足的语法，真难用，不知道学长学姐是怎么学的，而且竟然还发了论文，希望Z3可以替代它，我就不用在Coq的学习上花太多功夫了。
Kind2：也是一种验证软件，本地只支持linux和mac，竟然不支持windows，不知道开发人员是何许人也，幸好有网页版，勉强可以玩玩，但感觉自带的验证方式不必我自己用java写的来的快。
octave：跟吴恩达学机器学习时用的软件，很不错，绘图超快，自带的函数也能计算各种数学问题，和python差不多，但终归是差点，玩玩挺好，只是时代在变，以后可能还是以python来实现机器学习为主。