ljt12138的博客

博客

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会被高亮显示。如果你真的想打“@”这个字符，请用“@@”。