Vláďa Sedláček & Jonatan Kolegar

Vzdělání

Společnost

Osobní rozvoj

Věda a technika

Matematika

Filosofie

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

Místo problémů

Neformální podcast o přemýšlení, řešení problémů, abstrakci a netradičních úhlech pohledu pro všechny, kteří se nespokojí s jednoduchým vnímáním světa. 

Varování: Může obsahovat netriviální množství humoru a matematiky, někdy i kombinovaně (expertíza v těchto oblastech však není očekávaná).

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č: <a href='https://www.startovac.cz/patron/misto-problemu/'>https://www.startovac.cz/patron/misto-problemu/</a>
FB stránka: <a href='https://www.facebook.com/mistoproblemu'>https://www.facebook.com/mistoproblemu</a>
Web: <a href='https://www.mistoproblemu.cz/'>https://www.mistoproblemu.cz/</a>
 
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: <a href='https://github.com/ah1112/synthetic_euclid_4'>https://github.com/ah1112/synthetic_euclid_4</a>
- Lean blog post series: <a href='https://www.vladasedlacek.cz/en/posts/lean-01-intro'>https://www.vladasedlacek.cz/en/posts/lean-01-intro</a>
- Spherical triangles: <a href='https://en.wikipedia.org/wiki/Spherical_trigonometry'>https://en.wikipedia.org/wiki/Spherical_trigonometry</a>
- The Erdős Institute: <a href='https://www.erdosinstitute.org/'>https://www.erdosinstitute.org/</a>
- Blog of Alice Silverberg: <a href='https://numberlandadventures.blogspot.com/'>https://numberlandadventures.blogspot.com/</a>
- 3Blue1Brown: <a href='https://www.3blue1brown.com/'>https://www.3blue1brown.com/</a>
- Numberphile: <a href='https://www.numberphile.com/'>https://www.numberphile.com/</a>
- Project Euler: <a href='https://projecteuler.net/'>https://projecteuler.net/</a>
- Cryptohack: <a href='https://cryptohack.org/'>https://cryptohack.org/</a>
- Better explained: <a href='https://betterexplained.com/'>https://betterexplained.com/</a>
- Brilliant: <a href='https://brilliant.org/'>https://brilliant.org/</a>

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č: <a href='https://www.startovac.cz/patron/misto-problemu/'>https://www.startovac.cz/patron/misto-problemu/</a>
FB page: <a href='https://www.facebook.com/mistoproblemu'>https://www.facebook.com/mistoproblemu</a>
Web: <a href='https://www.mistoproblemu.cz/'>https://www.mistoproblemu.cz/</a>
 
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: <a href='https://github.com/ah1112/synthetic_euclid_4'>https://github.com/ah1112/synthetic_euclid_4</a>
- Lean blog post series: <a href='https://www.vladasedlacek.cz/en/posts/lean-01-intro'>https://www.vladasedlacek.cz/en/posts/lean-01-intro</a>
- Spherical triangles: <a href='https://en.wikipedia.org/wiki/Spherical_trigonometry'>https://en.wikipedia.org/wiki/Spherical_trigonometry</a>
- The Erdős Institute: <a href='https://www.erdosinstitute.org/'>https://www.erdosinstitute.org/</a>
- Blog of Alice Silverberg: <a href='https://numberlandadventures.blogspot.com/'>https://numberlandadventures.blogspot.com/</a>
- 3Blue1Brown: <a href='https://www.3blue1brown.com/'>https://www.3blue1brown.com/</a>
- Numberphile: <a href='https://www.numberphile.com/'>https://www.numberphile.com/</a>
- Project Euler: <a href='https://projecteuler.net/'>https://projecteuler.net/</a>
- Cryptohack: <a href='https://cryptohack.org/'>https://cryptohack.org/</a>
- Better explained: <a href='https://betterexplained.com/'>https://betterexplained.com/</a>
- Brilliant: <a href='https://brilliant.org/'>https://brilliant.org/</a>
- Khan Academy: <a href='https://www.khanacademy.org/'>https://www.khanacademy.org/</a>

Aplikace Youradio Talk

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

Poslechněte si podcast