28: André Hernández-Espiet - Euclid, employment and education
Description
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/
United States
