Knitting & Lean (1/31/25)

Knitting Dreams

I've recently been considering learning to knit. It feels like it could be a productive way to distract myself and manage my anxiety. I can picture myself knitting in the back of a lecture hall while listening to talks, knitting in my chair while pondering math problems, and knitting on the bus while enjoying an audiobook. Moreover, I need something to replace endless doom-scrolling and struggling to write. Plus, imagine all the scarfs!

Unfortunately, I haven’t yet managed to find yarn and knitting needles. But, as it turns out, I stumbled upon something else to keep me occupied.

Learning Lean

Earlier this week, I found myself in a cramped Uber with a group of mathematicians on our way to dinner. During the ride, a few of them joked about writing a math book or paper where every theorem included a link to a Lean program. At the time, I had no idea what Lean was—my familiarity with proof assistants was nonexistent. They mentioned that Lean has online resources to help people learn it.

The next day, I was still without yarn or needles, so I decided to give Lean a try. I discovered the Lean Game Server and started with the Natural Number Game. It has been a refreshing distraction. The early levels reminded me of my first programming and proof-writing classes—I miss that sense of wonder and confusion that comes with learning a new language or rediscovering a basic proof. While I occasionally got frustrated by the limited instructions and wished for more straightforward examples, the experience has been a nice mix of fascination and frustration.

I don’t see myself becoming an enthusiastic champion for proof assistants yet, but I will keep learning. While I appreciate the concept of building a vast library of proofs, I don’t think I have the time or energy to commit fully to becoming a master of Lean and helping to translate older proofs. I think I’m better equipped and more motivated to help in development of libraries for SageMath or Networkx. But for now, I’m going to keep learning Lean—and who knows? Maybe one day, I’ll write a paper where every claim has a Lean proof.

Math Thought

The following applet is inspired by a talk I saw today by Peter Winkler on his paper Leading All The Way. Given a symmetric distribution one can generate a permutation of length n by taking n samples from the distribution, looking at the partial sums, and then adding the move i -> j if the ith partial sum is the jth smallest partial sum. Note, this is not a uniform distribution of permutations but it does have several nice properties (See Paper).