Math Talk! Dr. Andrej Bauer Explores Proof Assistants, Constructive Math, and Philosophy 🧠

In this wonderful discussion with Dr. Andrej Bauer we discuss a whole host of topics centering around constructive mathematics, and proof assistants.

Support Ukraine through Shtab Dobra:
Instagram: https://www.instagram.com/shtab.dobra/
Facebook: https://www.facebook.com/shtab.dobra
PayPal: bf.shtabdobra@gmail.com
etransfer: pochtanasha@gmail.com

The 5 stages of accepting constructivism:
https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf
Drawing + proof assistants:
https://homotopy.io/
https://www.eff-lang.org/
Is Dr. Bauer a constructivist?
https://math.andrej.com/2012/10/03/am-i-a-constructive-mathematician/
Propositions as [Types]:
https://academic.oup.com/logcom/article-abstract/14/4/447/933532?redirectedFrom=fulltext

Supporting Ukraine (0:00)
Introduction & discovering mathematics (1:52)
HoTT & Voevodsky (11:10)
AI (17:50)
Constructivism & plurality (23:35)
Proof assistants (32:50)
Folk knowledge (41:49)
The future of proof & implicit knowledge (47:50)
Philosophy (1:02:40)