It's summer and I've been back in the bay for about a week now. After a spring full of highs of low 50's in Madison, it's finally nice to consistently be able to enjoy low-70s weather. It has been a bit of a busy week, with my short trip to vancouver and catching up with friends I haven't seen in a while, but now that I am more settled down, I feel a bit empty. For the past semester I had enjoyed the luxury of having my goals laid out in front of me, even if I hadn't been very motivated towards some of them. It's over the summer when I don't have those extrinsic goals where I feel the most like I need that structure in my life. I sometimes wonder if that makes me somehow impure or inadequate. Yesterday I was at a Thai restaurant for lunch and I suddenly had a wave of emotion wash over me, that I needed to be doing something.
My new project is trying to formalize Furstenberg's proof of Szemerédi's Theorem in lean. I've been meaning to learn lean for a while, and I just gave a presentation on the proof, so I thought it would be a good opportunity to learn a new paradigm. So far my impression is moderately positive (although I haven't really done much with other theorem provers in the past). I do have a few qualms: the Mathlib4 docs are garbo, and Mathlib4 itself is missing a few definitions which would be useful for proving anything in Ergodic Theory (the weak limit, for one). I'm still at the stage where I'm stumbling over tactics and forgetting when I should use apply versus exact versus rw and so on, but I'm hoping that I'll get the hang of things soon.
That's all for now. I'm still mustering the courage to write about Mishima - maybe one of my next tidbits will be my thoughts on his work.