André Hernández-Espiet formalizes Euclid's Elements in the proof assistant Lean. He will offer some thoughts on:
- what principles are essential when coding up geometry in a rigorous way
- why is graduate school a scam
- which skills and approaches are useful both in academia and the industry
- how can early access to education influence your life
Startovač: https://www.startovac.cz/patron/misto-problemu/
FB page: https://www.facebook.com/mistoproblemu
Web: https://www.mistoproblemu.cz/
Timestamps:
(0:00) introduction
(3:49) Lean and getting into it
(7:20) axiomatic systems and different geometries
(19:33) practical aspects and benefits of using Lean
(34:56) Lean communities and communication across fields
(47:23) decoupling of math from its applications
(55:38) thoughts on grad school and transitioning to the industry
(1:05:51) networking and nepotism
(1:17:46) impact of math on personal life
(1:29:18) growing up in Puerto Rico
Links:
- André's formalization of the first book of Euclid's Elements: https://github.com/ah1112/synthetic_euclid_4
- Lean blog post series: https://www.vladasedlacek.cz/en/posts/lean-01-intro
- Spherical triangles: https://en.wikipedia.org/wiki/Spherical_trigonometry
- The Erdős Institute: https://www.erdosinstitute.org/
- Blog of Alice Silverberg: https://numberlandadventures.blogspot.com/
- 3Blue1Brown: https://www.3blue1brown.com/
- Numberphile: https://www.numberphile.com/
- Project Euler: https://projecteuler.net/
- Cryptohack: https://cryptohack.org/
- Better explained: https://betterexplained.com/
- Brilliant: https://brilliant.org/
- Khan Academy: https://www.khanacademy.org/
29: Julián Hernández-Serrano - science, survival, and storytelling
27: Ian Jauslin - crystals, complications, and curiosity
26: Jitka Petřeková - předci, paměti a politika
25: Karolína Bretová - myši, mozky a medicína
24: Tereza Agnes Pokorná - budování, bonita a bungalovy
23: Valdemar Švábenský - PhD, pedagogika a příprava
22: Lenka Knapová - rovnováha v pohybu, výzkumu i životě
21: Bonus - Sociální sonda na Noci vědců
20: Genealogie aneb rozrody, vývody a výhody
19: Myšlenkový pokus - magické patero
18: Tomáš Novotný, Tereza Kinská - kostky jsou vrženy, dejte si Bacha
17: Tran Anh Minh - kreslení, kreativita a kultury
16: Tomáš Perutka - abstrakce už pro mě ztratila význam
15: Jana Sotáková - překážky, podpora a piedestaly
14: Martin Ukrop - reflexe ve škole i mimo ni
13: Bonus - ohledy a výhledy
12: Jan Plhák - nejdřív zplodiny, potom plodiny
11: Radek Suchánek - křivé geometrie a červí díry nejen ve fyzice
10: Nina Kadášová - biofyzik může dělat cokoli, jen je potřeba ho zaučit
Create your
podcast in
minutes
It is Free
Breaking Math Podcast
The Universe Speaks in Numbers
Casual Inference
My Favorite Theorem
Opinionated History of Mathematics