Frankly speaking ...

Using Lean 4 for Mathematics Proofs In the previous post, I explored Lean 4 as a functional programming language. If you already know functional languages like Haskell, you will recognise a lot of familiar ideas. Where Lean starts to feel different is in its annotations and, especially, in its use of tactics with dependent types. To make that concrete, I will walk through a small mathematical proof in Lean 4. The goal is to show an irrationality result. The classic classroom example is that  2 – √  is irrational, but that proof needs extra machinery. Here, I will use a simpler example that only needs basic arithmetic. I will start with the maths proof, then translate the same idea into Lean 4. I like this proof because it is compact. It is the classic “one side must be even, the other must be odd” contradiction. Mathematics: Prove that  log 2 ( 3 )  is irrational I start by assuming  log 2 ( 3 )  is rational. That means there exist positive integers...