In my last post I described a style which uses Subtype as a return type in order to merge the primary theorem about a function with its type signature. If I use this style for my own code, my functions will take inputs of some arbitrary types, but always return a Subtype as a final result. And when writing new code I will want to combine such functions by applying one to the result of another. More precisely, given a value of type Subtype p_α, with p_α : α → Prop, and a function f : α → Subtype p_β , with p_β : β → Prop, I want to get a result of type Subtype p_β‘, for some suitable[…]
I haven’t posted a new article since my previous post on Fibonacci numbers. I found the idea of proving the correctness of my function highly tantalizing, but also more cumbersome than necessary. So I started working on some code which would help me prove statements about functions. This has absorbed the entire time I spend with Lean since then and I haven’t solved any additional Euler problems yet. This post describes the starting point of my journey. The standard style which I find in Mathlib is to write functions with functional code, just like I would in Haskell, and have separate theorems about properties of these functions with proofs. This is the style which I also used for the Fibonacci[…]
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”[…]
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[…]
The wise teacher is gazing absentmindedly out of the window. Finally she asks: “Why did some people believe that the Earth is flat?” After a short pause one of her pubils responds: “Well, it does look like the Earth is flat.” “Oh”, she responds in slight amazement, “Imagine we were living on a spherical Earth. I wonder that would look like” I don’t remember where I read this joke and I don’t think that on the very rare occastions I have told it anybody ever found it even funny. And yet I consider it the most supreme joke I have ever come across. Not only do I personally find it funny, but it also offers the hint of an answer[…]
Board Game Geek is an awesome resource for finding new interesting board games. There is however one shortcoming I have run up against more than once. When looking for a game for a specific player count, the available search filters and sort options are not very useful. I finally decided to tackle this myself based on the following idea. Board Game Geek includes a poll which lets users vote for a given player count to be the best, recommended, or not recommended. Under the assumption that votes for “best” and “recommended” reflect the Board Game Geek rating and that “not recommeded” reflect a rating of 2, we can compute an adjusted rating as To adjust for polls with a small[…]