Related: Terrence Tao discussing Lean (programming language for formalising mathematical proofs) on Lex podcast (starts 1h20m): https://www.youtube.com/watch?v=

Related: Terrence Tao discussing Lean (programming language for formalising mathematical proofs) on Lex podcast (starts 1h20m): https://www.youtube.com/watch?v=HUkBz-cdB-k&t=1h20m10s https://www.youtube.com/watch?v=HUkBz-cdB-k&t=1h20m10s I know nothing of mathematics but found it fascinating, especially the idea that if outside information changes that affects your proof, you can have the Lean compiler figure out which lines of your proof need updating (instead of having to go over every line, which can take days or more).