Imagine this: you’re excited about a new feature idea. You meticulously set up an A/B test to validate it. The results are in! Your new feature is a winner, boasting a statistically significant improvement in user engagement. Confidently, you roll it out to everyone, expecting to see those engagement metrics soar. But… the needle barely moves. Or worse, engagement slightly dips. Disappointing, right? If this scenario sounds familiar, you’re definitely not alone. Many businesses, across all industries, are bumping into a frustrating reality: A/B tests, despite their reputation for providing clear data-driven answers, often overstate the real-world impact of changes. Those seemingly definitive “winning” test results can feel misleading, leading to inflated expectations and real-world letdowns. We invest in A/B[…]
Note: This is part of my exploration of using AI for writing articles. I have described the process I’m using in Tired of “AI Slop”?. This explores the extent to which AI can understand the correctness of statements that contradict the dominant public opinion, which is critical for creating a truly insightful article. When you ask an AI a question, how confident can you be in the answer’s factual accuracy? A seemingly simple question – “Are dolphins fish?” – reveals a surprising complexity and highlights both the impressive abilities and critical limitations of current artificial intelligence when it comes to getting to the truth. Ask a typical AI model today: “Are dolphins fish?” and you’ll likely get a confident “No!”[…]
Note: This article is self referential. I used the process described here in order to create this article utilizing “Gemini 2.0 Flash Thinking Experimental with apps” (with the exception of this note) Artificial intelligence is amazing at writing. Need a product description? A social media post? AI can churn it out in seconds. But let’s be honest, sometimes AI-generated content feels… bland. Generic. Like it’s missing that spark of real insight. We call it “AI slop” – and we’re all getting a bit tired of it. But what if there was a way to use AI to write articles that are actually interesting, insightful, and original? What if you could partner with AI to create content that goes beyond the[…]
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[…]