hackertube.io

The Future of Mathematics?

Microsoft Research · talk · Watch on YouTube

Logic & formal methodsPure mathematics

What it is

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.

Why Hacker News recommends it

Recommended as the clearest mathematician's perspective on formal proof assistants and why mathematics should be formalized.

  • 9 people recommended it
  • 7 different months
  • 0 strong recommendations
  • first 2019, last 2025

What HN commenters said

  1. “seems pretty interesting”

    Kevin Buzzard talks about using the Lean theorem prover.

    stephenSinniah, 2019-10 · Recommendation · in “Learning How to Prove: From the Coq Proof Assistant to Textbook Style”

  2. “an interesting talk by Kevin Buzzard [1] from Imperial College London about how he wants to formalize all mathematics with theorem provers”

    Buzzard on formalizing mathematics and teaching proofs with Lean.

    infogulch, 2019-10 · Recommendation · in “Alloy is a language for describing structures and a tool for exploring them”

  3. “For a perspective of a mathematician that came to evangelize theorem provers, I recommend Kevin Buzzard's MS 2019-09 presentation [0] about LEAN.”

    Mathematician evangelizing theorem provers, covering cultural gaps and teaching with Lean.

    Nzen, 2019-10 · Recommendation · in “A Code Glitch May Have Caused Errors in More Than a Hundred Published Studies”

  4. “Got me to go back and re-watch Kevin Buzzard's talk at MS Research”

    Worth re-watching Buzzard's Lean talk.

    carapace, 2020-11 · Recommendation · in “Building the Mathematical Library of the Future”

  5. “I recently watched a talk about the Future of Mathematics[0] with respect to theorem proving and formalization.”

    Talk on future of mathematics with theorem proving and formalization.

    andrewnc, 2021-05 · Recommendation · in “Z3 Tutorial”

  6. “wanted to drop a link to buzzard's very interesting talk”

    Buzzard discusses fragility of mathematics and the role of elders.

    oolonthegreat, 2021-07 · Recommendation · in “Some stuff I found interesting about number theory research”

  7. “Here's a great video about a popular formal verfication proof assitant”

    Mathematician enthusiastic about using computers for proofs, tongue-in-cheek.

    liups, 2021-12 · Recommendation · in “The year in math and computer science”

  8. “Kevin Buzzard (a professional mathematician) has a few good talks about Lean”

    One of Buzzard's good talks about Lean.

    pas, 2023-10 · Recommendation · in “Lean4 helped Terence Tao discover a small bug in his recent paper”

Excerpts from Hacker News comments, linked to the originals. Summaries and labels were written by a language model from those comments.

Topics: lean, theorem proving, kevin buzzard, formalization, proof assistants

Also recommended by the same people