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/mistoproblemuWeb: https://www.mistoproblemu.cz/ Timestamps:(((((((((( 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/