Skip to content
0:00 / 0:00

#constructivemathematics#intuitionisticlogic#homotopytypetheory

Five Stages of Accepting Constructive Mathematics - Andrej Bauer

Institute for Advanced Study

161K subscribers • 3 videos on Hallway

YouTube
  • Recommended by 1 person: 1 on Hacker News.
  • Presented by Andrej Bauer, Member of the School of Mathematics

Advanced. Deep dive for people who know the field.

33K views10 years ago1 recommendation

Computer scienceComputation and complexityFormal methods and verification

Andrej Bauer introduces constructive mathematics and explains what it is like to do mathematics without the law of excluded middle.

Andrej Bauer University of Ljubljana, Slovenia; Member, School of Mathematics March 18, 2013 Discussions about constructive mathematics are usually derailed by philosophical opinions and meta-mathematics. But how does it actually feel to do constructive mathematics? A famous mathematician wrote that "taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists." Was he right? In this talk we shall visit the astounding worlds of constructive mathematics. As tourists from the classical world we will at first be shocked by the bizarre and unfamiliar phenomena, but hopefully also left curious about the new possibilities and dimensions of mathematics that the classical dogma declares heretical or even non-existent. For more videos, visit video.ias.edu

Why it's here

1 person recommends this

What people say. Recommended as an engaging and accessible introduction to constructive mathematics and logic.

jimhefferonon Hacker News • Recommends

On “The weird and wonderful world of constructive mathematics (2017) [pdf]”

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 link to this video , and a paper link (sorry, the paper link may not work for everyone, but the video contains basically the same content.)

no_identdon Hacker News • Mentions

On “Unprovability comes to machine learning”

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 th…

leonidasrupon Hacker News • Mentions

On “"Why not just use Lean?"”

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. link to this video link

u/barsoapin r/compsci • Mentions

On “What are the basic assumptions of type theory-based proof assistants compared to those of traditional mathematics (e.g. real analysis)?”

Constructivism. All those systems are constructivist because a) necessity and b) written by CS folks. Have a lecture, "Five Stages of Accepting Constructive Mathematics", as well as the HoTT book. Covers the reals at least to some degree, with some luck you'll find the rest of real analysis elsewhere.