HackerTube.dev

The Future of Mathematics?

Microsoft Research · 116.1K views · 2019-10-01 · 1:14:48

Open on YouTube ↗

If playback is restricted in your region, try opening the original video. Use Mark watched to add it to your marked videos.

Overview

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.

On Hacker News

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

Recommended by 9 HN people across 7 months · HN mentions 2019–2025

Topics

Logic & formal methodsPure mathematics
Search by tags
leantheorem provingkevin buzzardformalizationproof assistants

What people said

ookdatnog · 2025-08 · Recommendation

I watched this video years ago and found it interesting. It's a talk by Kevin Buzzard, a pure mathematician who got really interested in theorem proving software, and he explains his motivation. [VIDEO]

Read the original HN comment ↗
pas · 2023-10 · Recommendation

Kevin Buzzard (a professional mathematician) has a few good talks about Lean [VIDEO] from 2019 at MS Research [LINK] (2022 at ICM international math congress)

Read the original HN comment ↗
liups · 2021-12 · Recommendation

> pure math (topology and countability) and computer science have almost no overlap in the short term. This is an unexpected opinion. What do you mean by this? I would argue the opposite. Look at Formal Verification[0]. Here's a great video about a popular formal verfication proof assitant: [VIDEO] A quote from the mathematician in the video expressing enthusiasm for using computers for mathematics: "All I want to do... I don't want to do mathematics on pen and paper anymore, because I don't trust it, and I don't trust other people that use it; which is everyone." (in case people only read this quote, instead of watching the lecture, the tone is tongue-in-cheek) Formal Verification would seem a literal intersection of pure math (formal proofs[1]) and computer science (formal specification[2]). Of note, one of the popular underlying foundations of an approach to formal verification is Homotopy Type Theory(HoTT)[3][4] which is an asserted effort to show the relationship between type theory and, specifically, topology (homotopy[5]). [0] [LINK] : fancy word for 'computer verified mathematical proofs' [1] [LINK] : fancy word for 'proof' [2] [LINK] : fancy word for 'rules for an algo that checks a proof' [3] [LINK] [4] [LINK] : a great read, even if you are a novice, or prefer other formal verification foundations [5] [LINK] : "It originated as a topic in algebraic topology"

Read the original HN comment ↗

Sources

Video by Microsoft Research, played through YouTube.

Data and selection notes

HN summaries and labels may contain AI errors. HN dates refer to discussions, not video publication.

HN Library: HackerTube export (2026-10-31) and open-index/hacker-news. Upstream summaries and classifications may contain AI errors.

Views, duration and playback status refresh separately from the published catalog. When an update fails, existing data remains visible.

Selection checks
  • SaaS & AI candidates: Topic keywords do not match
  • Editor-approved picks: Editorial review is required

Rule matches identify candidates. They do not guarantee video quality or financial results.

About the library and its sources