At timestamp 30:00 he talks about hyperlinked drill down proofs, as the format of textbooks of the future. Leslie Lamport begged everyone to do this 7 years ag

At timestamp 30:00 he talks about hyperlinked drill down proofs, as the format of textbooks of the future. Leslie Lamport begged everyone to do this 7 years ago (paper and video linked from blog post [1]), based on his TLA-backed speech on a similar topic 30 years ago [2] and I'm sure it goes back further. Proof wiki also does this, in part. [1] https://aperiodical.com/2017/09/hlf-blogs-leslie-lamport-thinks-your-proofs-are-bad/ https://aperiodical.com/2017/09/hlf-blogs-leslie-lamport-thi... [2] https://www.microsoft.com/en-us/research/publication/how-to-write-a-proof/ https://www.microsoft.com/en-us/research/publication/how-to-... Aside, it's encouraging to see that someone with poor public speaking ability can still become a top mathematician and mathematical writer.