jimhefferonon Hacker News • Recommends
On “The weird and wonderful world of constructive mathematics (2017) [pdf]”
#constructivemathematics#intuitionisticlogic#homotopytypetheory
161K subscribers • 3 videos on Hallway
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.eduWhat 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]”
no_identdon Hacker News • Mentions
On “Unprovability comes to machine learning”
leonidasrupon Hacker News • Mentions
On “"Why not just use Lean?"”
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)?”