UOJ Logo ljt12138的博客

博客

NOI2020 D2T2 Surreal 主定理的一个形式化证明

2020-09-05 10:27:09 By ljt12138

最近试玩了一下一个叫做 Lean 的定理证明器,并尝试在里面证明了 Surreal 的主定理:一个树的集合是完备的当且仅当它能够生成每一棵高度为 $h$ 的树,其中 $h$ 为树的集合中包含的最高的树的高度。整个证明大概有 1k lines,花了大约 15 小时。

证明放在这里,欢迎大家来验证/基于里面的定理继续搞事

(正在考虑要不要冬令营来做一个关于定理证明器的 talk hh)

评论

saffah
https://github.com/ljt12138/ljt12138.github.io/blob/master/files/problems/noi20_report.pdf 好像挂了,文件大小是 0 Byte
Picks
nb啊,有对Coq感兴趣的童鞋吗

发表评论

可以用@mike来提到mike这个用户,mike会被高亮显示。如果你真的想打“@”这个字符,请用“@@”。