I am fascinated by Lean 4, because it looks like a great programming language and on top of this it also provides the facilities for proving theorems about code written in this language. Today, in a typical software engineering project, I would define a custom structure, to represent a concept, i.e. I have a network of interdependent tasks, which need to be run under certain circumstances. Usually there are some requirements on the state of this structure, such that it makes sense based on this concept, i.e. the tasks have lists of upstream and downstream tasks and a tasks needs to be in the downstream list of each of the tasks in its upstream list. These are called “(class) invariants”[…]
Tag: Project Euler
Problem 3: Largest prime factor This problem proved to be a quick snack for Lean 4, and I was able to solve it with a quick call to the library function Nat.factors. Revisiting Problem 2: Even Fibonacci numbers After solving problem 3, I decided to have a closer look at some of the types I found while looking for a solution for problem 2. I realized that I could use very similar code to the one I used for my Stream instance, to construct members of type Stream’, Stream’.Seq, and Stream’.WSeq. I realized that Stream’.Seq.corec used the same construction, that I had used for my FibStream, so the following creates a Stream’.Seq ℕ. This is one instance where I found[…]
Problem 2: Even Fibonacci numbers Fibonacci numbers are a common toy problem which is used in many programming tutorials, since naive implementations can go horribly wrong. Mathlib of course contains an implementation, which avoids all these pitfalls, and an even faster implementation. I didn’t use either for this problem for multiple reasons. First, when I started this problem I didn’t know about the Mathlib4 docs, so I wasn’t even able to find them. Second, since I want to learn Lean 4, it’s a reasonable exercise to implement it myself. And third, I don’t actually want a function which gives me the n-th Fibonacci number, I want a function which gives me all the Fibonacci numbers up to the n-th. This[…]
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[…]