Friday Nov 10, 2023

28: André Hernández-Espiet - Euclid, employment and education

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



FB page:




(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



- André's formalization of the first book of Euclid's Elements:

- Lean blog post series:

- Spherical triangles:

- The Erdős Institute:

- Blog of Alice Silverberg:

- 3Blue1Brown:

- Numberphile:

- Project Euler:

- Cryptohack:

- Better explained:

- Brilliant:

- Khan Academy:

Comments (0)

To leave or reply to comments, please download free Podbean or

No Comments

© Místo problémů 2023. Všechna práva vyhrazena.

Podcast Powered By Podbean

Version: 20240320