几个数学机械化程式

Jgex (java geometry expert) 已上架snap
https://github.com/kovzol/Java-Geometry-Expert
可以当几何画板，可以数值检验，使用包括吴方法的多种机器证明方法自动证明，还能生成很短很简洁的可读证明，当初数学文化上听说了吴方法，在数学机械化实验室看到了一些半成品，GitHub上这个项目现在还有人维护，数学机械化实验室里好多都是deadlink，还有一个maple wsolve包

机械化实验室的软件http://mmrc.amss.cas.cn/kycg/cbwyrj/rj/

里面还开发了数学机械化自动推理平台，这个还不是deadlink，可以试试
http://www.mmrc.iss.ac.cn/mmp/index.htm

BOTTEMA 几何不等式自动发现证明
https://nguyenhuyenag.wordpress.com/software/
是一个maple包，上面的链接还有sos的maple包和叫psdgcd的不等式自动证明和解决优化问题的包

prover9 and mace4 一阶逻辑和等词逻辑自动证明和举反例，语法简单，gui界面
https://www.cs.unm.edu/~mccune/prover9/

自动定理证明器博物馆
https://theoremprover-museum.github.io/

yhtq

挺有意思2333 感谢！

Mathematica analytica可以自动证明数分问题，没试过

https://library.wolfram.com/infocenter/Articles/3152/#:~:text=Analytica is an automatic theorem prover written in,beyond the scope of previous automatic theorem provers.

https://vprover.github.io/

vampire自动证明器似乎是逻辑系列最强的了