28: André Hernández-Espiet - Euclid, employment and education Místo problémů

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/