name the biggest number 源码

最大的名字 该存储库的目的是使人们可以提交具有最大数量头衔的竞争者。 本次比赛的想法是由斯科特·阿伦森描述,但通常这是趣味数学的一个非常活跃的地区,很多资源都可以找到。 该存储库为流程增加了两个警告: 所描述的数字必须是建设性的:没有繁忙的海狸或类似的恶作剧! 原则上,所有命名的数字都必须是可计算的(稍后会详细介绍)。 提交的数字必须在Coq规范系统中进行正式描述,并提供正式的证明,证明其数量大于当前最大数量的竞争者。 一些基本规则: 在“合理”的机器上使用coqc进行数字检查时,数字的定义必须不超过15秒。 该数字大于当前竞争者的证明应该花费不超过1分钟的时间来进行类型检查,不过我可能会根据事件需要对此进行更新。 没有公理! 如果需要,可以包括图书馆,但请尝试使用广泛使用的图书馆。 通过根据该文件概述的格式制作一个添加到文件Contender.v的PR(您的编号应为名为