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/