2020-6-14 11:5莱昂纳多·达·芬奇当然以他的绘画和素描而闻名,但他也对发明感兴趣,并对包括数学和工程在内的科学的各个领域感兴趣。考虑到他对我们这个世界的持续影响,很难想象他在500多年前就去世了。他发明了实用和不切实际的发明:乐器、机械骑士、液压泵、可逆曲柄机构、翅片迫击炮和蒸汽炮。
你可能会问:打样机和永动机有什么共同之处?证明是......
2020-5-2 17:51一段时间以来,我一直在考虑举办一系列名为“万能证明助手”的研讨会,专门针对所有不同的证据助手。除了现有的助手(Isabelle/HOL,CoQ,AGDA,Lean)之外,还有其他有趣的实验验证助手,还有一些还在开发中,或者只是概念的证明。我想更多地了解他们,我想我不是唯一的一个。
让证明助理的作者前往卢布尔雅那,并在......