【英字】The Future of Mathematics?IMO满分得主、代数数论专家力推定理证明器

1931
7
2019-10-18 09:19:21
60
21
112
23
Kevin Buzzard 是 1987 年 IMO 满分得主,如今是一位代数数论专家。Kevin 于 2017 年开始接触交互式定理证明器 Lean Prover,通过亲身体验和教学实验,Kevin 成为定理证明器的信徒和布道者,坚信它们会改变数学研究的未来。Kevin 分享了自己学习定理证明器从挫败到依赖的过程,分享了自己被数学专业本科生超越的故事,介绍了他们目前所做的工作和长期的计划,还从职业数学家的角度发表了对形式验证未来发展的看法。更多关于讲座、讲师、课件的信息参见置顶评论。
  • 字幕制作者(English):fracting
欢迎加入形式验证交流群,微信fracting
接下来播放
自动连播
客服
顶部
赛事库 课堂 2021拜年纪