My background

I’m a Data Scientist with a degree in Mathematics. I mostly write in Python these days, but in the past I have extensively used R and Ruby, and I have dabbled in quite a few other languages. The language most relevant to this project is probably Haskell. Not only is it a rather pure functional programming language like Lean 4, but I also learned it by working on project Euler. Of course that was more than 10 years ago, and I never got a chance to use it in a professional setting.

Lean 4

I’ve been fascinated by proof checkers and theorem provers for a very long time, but none of the solutions I have found in the past felt quite right to me. When I researched this topic once again recently, I found Lean 4, which proclaims itself to be “a functional programming language that makes it easy to write correct and maintainable code” and also “an interactive theorem prover”. So I have decided to take it by its word and learn it as programming language

Project Euler

Project Euler is a website containing mathy problem sets, which can typically only be solved by using programming. I have used project Euler in the past, when learning a new programming language, to make sure I understand the language well enough to produce functional and reasonably efficient code to solve problems. I will do the same for Lean 4 and I have decided to blog about my progress.

Project Euler asks not to publish solutions to their problems, so I will not publish complete solutions to their problems. But I will talk about some principal ideas behind those solution and how to implement them in Lean 4. This is primarily about Lean 4, not about project Euler.

Setup

Using the VS Code plugin as described in the Lean 4 manual quickstart section worked quite well to get the language up and running. However the lake command didn’t work in the terminal, so I didn’t find a way to install Mathlib. After searching rather long for a solution, it got fixed when I restarted my computer.

Getting Mathlib and the project set up is described in more detailed in my second post in this series.

Documentation

Documentation is a weak point of Lean 4, which probably isn’t surprising, given how new the language is. The first official release 4.0.0 was published on Sep 8, 2023, which as of this writing was just three weeks ago.

Books

It was in development for some time and there are several book type resources available. Since, as of now, I’m primarily interested in Lean 4 as a programming language, I focused on Functional Programming in Lean. I found it quite understandable, though sometimes the example code used some features, which I didn’t remember reading about before. I also selectively read Mathematics in Lean, which, even though it focuses on proofs, contains relevant information on Lean 4 as a programming language. The Lean Manual also contains useful explanations, but as of now it contains large sections of empty space, interspersed with TODOs, which probably will be filled in at some point. All of these are linked from the Lean documentation page.

Mathlib4 docs

What is curiously lacking from the documentation page, is a link to the Mathlib4 docs, which extracts documentation from the source code, not only for Mathlib, but also for the base language itself, the standard library Std, and a couple of other libraries. I found this to be an indispensable reference when trying to code in Lean 4.

One big plus for Lean 4, at least from my perspective, is that the source code is, in most cases, very readable. So the ability to search, combined with the automatically generated links to “Instances” and “Instances For”, in combination with the type information and link to the source code, works very well for my needs.

Problem 1: Multiples of 3 or 5

Solving this problem was straight forward, even without Mathlib, or a functioning lake. The key component was to implement a function filtered_sum, which takes another function which filters natural numbers and an upper limit and produces the appropriate sum. I wrote it as a tail recursive function, as I remember from earlier excursions into functional programming, and as described in the books.

def filtered_sum (f: Nat → Bool) (n: Nat) : Nat :=
  let rec go (acc: Nat) : Nat → Nat
    | 0 => acc
    | n + 1 => if f (n + 1)
      then go (acc + n + 1) n
      else go acc n

  go 0 n

Rather than compiling and running the program, I just used #eval with the appropriate inputs

#eval filtered_sum divisible_by_3_5 9

That’s all for now. This series will continue with problem 2.