The Future of Mathematics?
9 人推荐 · 跨 7 个月 · 2019–2025
中文导读
数学家 Kevin Buzzard 阐述为什么他坚信 Lean 定理证明器将彻底重塑数学的未来。他分享了自己带领本科生用 Lean 将大学数学课程全盘数字化的实践，以及在传统数学界推行形式化验证面临的文化阻力。
为什么 HN 推它
被公认为从一线数学家视角阐述形式化证明助手及“数学为何必须形式化”最清晰通透的一场演讲。
「想了解一位投身定理证明布道的数学家视角，我推荐 Kevin Buzzard 2019 年 9 月在微软关于 LEAN 的演讲。」HN 网友原话：For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN.
英文原摘要（HackerTube / Claude 整理）
Mathematician Kevin Buzzard explains why he believes the Lean theorem prover will shape the future of mathematics, and describes digitizing his university curriculum in Lean with undergraduates, plus the cultural challenges.
Recommended as the clearest mathematician's perspective on formal proof assistants and why mathematics should be formalized.
HN 上的提及
seems pretty interesting
an interesting talk by Kevin Buzzard [1] from Imperial College London about how he wants to formalize all mathematics with theorem provers
For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN.
some mathematicians are advocating that mathematical proofs should be specified as code
YouTube comments by a Lean developer, cited as source.