It’s been 3 months since my previous post about learning Lean part 3, so it’s time to write another one. I have mostly continued to work through Tao’s Analysis book through his excellent companion - which means all proofs from the paper textbook are fully formalized in Lean, while examples and exercises are stated in Lean but left with a sorry for me to fill in. Altogether the companions has close to 2000 sorries to fill-in.| Rado's Radical Reflections