Math Talk! Dr. Andrej Bauer on proof assistants, constructive mathematics, philosophy, and more.

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)