zhtprog的个人博客分享 http://blog.sciencenet.cn/u/zhtprog

博文

有限群理论的机器证明

已有 2745 次阅读 2015-7-11 10:10 |个人分类:机器证明|系统分类:科研笔记| 机器证明

今天我刚完成了一个数学定理的机器证明,是有限群理论里的一个重要定理First Sylow Theorem。这个证明花了两个多月时间,因为使用的是一个新型的机器证明工具,很多基础工作都是从头做起。证明发在这里:https://github.com/htzh/leanproved

一共用了3317行代码,  21715个词, 134230个字符。实际上写的代码还多一些,有一部分已经放到标准库里去了。这一段时间真是做梦也想着这个工作,总算告一段落了!

我会写一个介绍这个机器证明思路的博文,正文会是英文的,但有时间的话也会写一点中文的介绍。这个定理的文字证明(机器证明的数学思路是建立在其上的)在这里:http://htzh.github.io/problemdriven/posts/Sylow.html

 




https://wap.sciencenet.cn/blog-2398747-904583.html

上一篇:小技巧:如何在博客的评论区使用数学符号?
下一篇:波尔兹曼方程的单粒子解
收藏 IP: 108.193.233.*| 热度|

该博文允许注册用户评论 请点击登录 评论 (0 个评论)

数据加载中...

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2022-12-3 06:11

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部