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
- Zdroj: VědaVýzkum.cz
- Audio url: https://open.spotify.com/embed/episode/2iLXe5ugo94ymi1pjS5ECR