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/