HackerTube.dev

Five Stages of Accepting Constructive Mathematics - Andrej Bauer

Institute for Advanced Study · 34K views · 2016-08-16 · 57:32

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

Andrej Bauer's IAS talk introduces constructive mathematics and what it feels like to do mathematics without excluded middle. It is framed as a tour for classical mathematicians.

On Hacker News

Pointed to as a well-done introduction to constructive mathematics when it comes up in logic and proof assistant threads.

Recommended by 1 HN people across 1 months · HN mentions 2018–2026

Topics

Logic & formal methodsPure mathematics
Search by tags
andrej bauerconstructive logicexcluded middletype theoryfoundations

What people said

jimhefferon · 2018-11 · Recommendation

There are a lot of folks here asking for a bit more. Here are two versions of the same well-done talk, from Andrej Bauer: a video [VIDEO] , and a paper [LINK] (sorry, the paper link may not work for everyone, but the video contains basically the same content.)

Read the original HN comment ↗
leonidasrup · 2026-04 · Reference

Five stages of accepting constructive mathematics: Denial Anger Bargaining Depression Acceptance A talk about constructive mathematics by Andrej Bauer at the Institute for Advanced Study. [VIDEO] [LINK]

Read the original HN comment ↗
no_identd · 2019-01 · Reference

That depends on what you mean by "Church-Turing thesis": * [LINK] The Interactive Nature of Computing: Refuting the Strong Church-Turing Thesis (Published version here: [LINK] ) * [LINK] See also a previous hacker news discussion of the Church-Turing thesis here: [LINK] albeit I take issue with the supposed "proof" by counter example via Compass & Straightedge construction given in the video there, due to results like these two: * [LINK] Kellison, Ariel; Bickword, Mark; Constable, Robert L. - Implementing Euclid’s straightedge and compass constructions in type theory [September 2018] (Code here: [LINK] ) * [LINK] (Numerous papers by Michael Beeson et al., just check the page, I won't link them all here) (Note that the authors of the two above works take very different yet similar approaches to the whole matter, it really pays off to compare both to each other.) However, there seem to exist at least two different spanners in the works: * [LINK] Makowsky, Johann A. - Can one design a geometry engine? On the (un)decidability of certain affine Euclidean geometries * [LINK] Makowsky, Johann A. - The Undecidability of Orthogonal and Origami Geometries (If the first of the two above papers makes you wonder "well who DIDN'T overlook Ziegler's theorem... Well... [LINK] ) Oh and in case anyone here still believes Hilbert's old wives tale about /his/ Axiom of Choice, there's plenty of AC to go around in constructive mathematics: [LINK] But if that doesn't convince you yet, you might go

Read the original HN comment ↗

Sources

Video by Institute for Advanced Study, 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