Lean, Lockdown and Languages

It's been a busy week. I've been coordinating the car parking at the local COVID-19 vaccination clinic. This particular clinic's aim was to complete the vaccination of all people of eighty years or older. The shifts went smoothly, pretty much a model of good cooperation, and I met some great people too. Today I've been responding to fairly heavy snowfall in Bradford-on-Avon, working in a team of four CEVs to clear a route of steep footpaths of just under 500m in length. People use these footpaths to get from the top of the town to its centre. Another team did a similar route on the other side of town. The aim was to stop the formation of black ice which would make those routes impossible to use safely, and can lead to injury for those that choose to anyway.

On Thursday I attended (virtually) my first Archimedeans talk in ages. In January 2016, I lived in Cambridge. Adam Forsythe-Cheasley came to visit me, and we went to a talk by Kevin Buzzard on the congruent number problem. It was clear, enlightening and enjoyable, so we went to Thursday's talk. The topic this time was what is meant by equality. He presented some ways that the opinions of different mathematicians from Euclid onwards have differed on the matter, and how to 'cheat' these definitions. At the end of the talk there was some discussion of the Lean theorem prover. Kevin Buzzard runs the Xena project, the goal of which is to get (undergraduate) mathematicians to learn to use proof verification software like Lean. He is also developing mathlib, a collection of theorems and definitions in order to help this to happen.

Early last year I was interested in interactive theorem provers and proof assistants like Coq and Isabelle, and in programming languages with dependent types like Idris. Lean 4 was released recently, and sounds like it has more of an emphasis on doing modern mathematics with a computer than Coq and Isabelle, which are, by comparison, perhaps more focussed on the needs of computer science. On the Discord server, Kevin mentioned that to prepare for working with Lean, he studied some of Learn You A Haskell for Great Good!, a book which served as my first introduction to Haskell. Lean is a functional programming language like Haskell, so hopefully my enthusiasm for it over 2020 will help me get into Lean. As well as this book, Theorem Proving in Lean is recommended as the standard reference.

But having said all this, The Natural Number Game is mentioned in all sorts of places as a starting point for exploring this world. One of these places is Learning Lean, which gives plenty of other paths to learning depending on your background and interests. The Natural Number Game is an interactive tutorial which concentrates on proving properties of elementary operations on natural numbers. The tutorial is structured as a series of levels to pass, structured into 'worlds'. As you progress, you prove more and more about the natural numbers, and, in doing so, appreciate the power of induction. I admit I haven't got very far with this yet, but that which I have completed I've enjoyed.

In other news, "Lockdown III" wears on, and I find that self-study is helping to distract me from it in a constructive way. I've always been really into (natural) languages. I've studied quite a few in my time. However, I've often skipped over some of the detail in order to save time getting to a basic level of communication, even if that communication is gramatically flawed. My goal for the end of 2021 is to go back to the start and study French, German and Spanish through to CEFR level B2. While doing this I'll try to learn every noun's gender so that I inflect properly, every irregular plural, every strange preposition and prepositional verb, every idiom, that I come across. The tool for this is Anki, a flexible flashcard app based on spaced repetition. As I study, I add electronic flashcards to a deck on my laptop and then sync it to the AnkiWeb service. When I sync my mobile Anki app, I can see these cards and study them. I use two kinds of card. Plain vocabulary cards prompt me with an English word and require me to remember the word, gender and plural to say I've remembered that world. The other type are fill-in-the-blank sentences in the studied language, also known as cloze deletion or cloze occlusion. Anki gives me twenty cards to study each day, scheduling the next review for ever-longer periods in the future as I internalise them. Over time, the flashcards will tend toward my understanding of the language as a whole, and the Anki will function as 'my brain in an app'. The method was recommended to me by a friend who speaks at least a dozen languages, and I myself have used it successfully in the past to get good scores on my radio exams.

Of course, while this covers the written language quite nicely, it's also important to practice speaking and listening. To this end, a friend and I have set up an electronic regulars' table = ein elektronischer Stammtisch. We hope that one day circumstances will mean that this can be an actual Stammtisch in Bristol, but for now we get together for a short chat on Wednesday nights at 20:00 UTC on the heathens.club Mumble server. Everyone learning German is welcome, as well as any native germanophones willing to help us out. Right now we only have learners and we're concerned we might reinforce each others' bad habits.

Reading back on all I've written this week, I realise how keen I am at the moment to learn and code, as well as to get outside and be useful somehow. I take this as a good sign of my own state of mind at a time when I know a lot of people are struggling. I know that I am fortunate to have the ability to do these things. Let's hope things get better for everybody soon.