博文
有限群理论的机器证明
|||
今天我刚完成了一个数学定理的机器证明，是有限群理论里的一个重要定理First Sylow Theorem。这个证明花了两个多月时间，因为使用的是一个新型的机器证明工具，很多基础工作都是从头做起。证明发在这里：https://github.com/htzh/leanproved
一共用了3317行代码， 21715个词， 134230个字符。实际上写的代码还多一些，有一部分已经放到标准库里去了。这一段时间真是做梦也想着这个工作，总算告一段落了！
我会写一个介绍这个机器证明思路的博文，正文会是英文的，但有时间的话也会写一点中文的介绍。这个定理的文字证明（机器证明的数学思路是建立在其上的）在这里：http://htzh.github.io/problemdriven/posts/Sylow.html
https://blog.sciencenet.cn/blog-2398747-904583.html
上一篇：小技巧：如何在博客的评论区使用数学符号？
下一篇：波尔兹曼方程的单粒子解
