《为什么的快乐
2022年7月5日
评论
“我认为，在这次合作中发生的一件事是，计算机科学家开始更多地了解现代数学的本质到底是什么样子的。”凯文的秃鹰
图片来源:Getty Images
在过去的几年里，世界各地的研究人员和业余爱好者共同努力，将数学的基本公理翻译成一种名为Lean的编程语言。有了这些知识，理解精益的定理证明程序已经开始帮助一些世界上最伟大的数学家验证他们的工作。
在一次采访中，伦敦帝国理工学院纯数学教授凯文·布泽德谈到了向利恩“教授”数学的努力——以及像这样的项目将如何塑造数学的未来。
从为什么的快乐
查看全文
没有找到条目
