# Lean golf: Pascal vs. Fibonacci

The Pascal's triangle and the Fibonacci sequence have an interesting connection: Source: Math is Fun - Pascal's triangle

Your job is to prove this property in Lean theorem prover (Lean 3 + mathlib). Shortest code in bytes wins.

import data.nat.choose.basic
import data.nat.fib
import data.list.defs
import data.list.nat_antidiagonal

theorem X (n : ℕ) :
((list.nat.antidiagonal n).map (function.uncurry nat.choose)).sum
= n.succ.fib :=
sorry -- replace this with actual proof


Since the statement itself depends on the current version of mathlib, it is encouraged to use Lean web editor (as opposed to TIO) to demonstrate that your answer is correct.

Some primer on the built-ins used:

• nat or ℕ is the set/type of natural numbers including zero.
• list.nat.antidiagonal n creates a list of all pairs that sum to n, namely [(0,n), (1,n-1), ..., (n,0)].
• nat.choose n k or n.choose k is equal to $$\_nC_k\$$.
• nat.fib n or n.fib is the Fibonacci sequence defined with the initial terms of $$\f_0 = 0, f_1 = 1\$$.

In mathematics notation, the equation to prove is

$$\forall n \in \mathbb{N},\; \sum^{n}_{i=0}{_iC_{n-i}} = f_{n+1}$$

## Rules

• Your code should provide a named theorem or lemma X having the exact type as shown above. Any kind of sidestepping is not allowed.

• The score of your submission is the length of your entire source code in bytes (including the four imports given and any extra imports you need).

• Do we have to use the provided code as a template, or can we start from scratch? Oct 8, 2021 at 0:09
• @cairdcoinheringaahing Starting from scratch is fine, as long as the statement being proved is correct. You need the four imports to just write down the statement though. Oct 8, 2021 at 0:12

# Lean, 299 bytes

import data.list data.nat.fib
open nat
def s(n k):=((list.nat.antidiagonal n).map$λa:_×_,choose(a.1+k)a.2).sum def X:∀n,s n 0=fib(n+1)|0:=rfl|1:=rfl|(n+2):=by{let:∀k,s(n+2)k=choose k(n+2)+s n k+s(n+1)k,induction n;intro;simp[s,(∘),<-add_one,add_assoc,*]at*;ring,rw[one_add,choose],ring,safe}  Try it on Lean Web Editor • a bit better with 468: import data.list data.nat.fib open nat def a:=@add_assoc def s(f:_->ℕ)(n):=((list.nat.antidiagonal n).map f).sum def A:∀(f:_->ℕ)n,(∀m,f(m,0)=1)->(∀m n,f(m+1,n+1)=f(m,n)+f(m,n+1))->s f(n+2)=f(0,n+2)+s f n+s f(n+1)|f 0 b c:=by simp[s,b,c,a]|f(n+1)b c:=by{let h:=A(f∘prod.map succ id)n,simp[s,c,a]at*,rw[h (λx,b$x+1)],simp[<-a],ac_refl}def X:∀n,s(λa,choose a.1 a.2)n=n.succ.fib|0:=rfl|1:=rfl|(n+2):=by let h:=A(λa,choose a.1 a.2);simp at*;rw[h,X,X];tauto (I'm not sure what the etiquette on basically changing existing answers is here) Oct 9, 2021 at 17:17
• you can also replace the imports with one to data.real.golden_ratio (because of transitive imports) but that's sadly the same length Oct 9, 2021 at 17:26
• oh, I'm not allowed to edit comments: here's 458:import data.list data.nat.fib def a:=@add_assoc def s(f:_->ℕ)(n):=((list.nat.antidiagonal n).map f).sum def A:∀(f:_->ℕ)n,(∀m,f(m,0)=1)->(∀m n,f(m+1,n+1)=f(m,n)+f(m,n+1))->s f(n+2)=f(0,n+2)+s f n+s f(n+1)|f 0 b c:=by simp[s,b,c,a]|f(n+1)b c:=by{let h:=A(f∘prod.map(+1)id)n,simp[s,c,a]at*,rw h(λx,b$x+1),simp[<-a],rw add_comm}def X:∀n,s(λa,a.1.choose a.2)n=(n+1).fib|0:=rfl|1:=rfl|(n+2):=by let h:=A(λa,a.1.choose a.2);simp at*;rw[h,X,X];tauto Oct 9, 2021 at 17:43 • open nat will lose some chars Oct 9, 2021 at 22:56 # Lean, 247 243 bytes import data.nat.fib data.list open nat list.nat def X:∀n,((antidiagonal n).map$function.uncurry
choose).sum=fib(n+1)|0:=rfl|1:=rfl|(n+2):=by

• Also 243 bytes is a finset version with the equality swapped: import data.nat.fib data.finset open nat finset.nat def X:∀n,fib(n+1)=(antidiagonal n).sum(λp,choose p.1 p.2)|0:=rfl|1:=rfl|(n+2):=by rw[fib_add_two,antidiagonal_succ_succ'];safe[X,antidiagonal_succ',choose_succ_succ,finset.sum_add_distrib] Feb 16 at 0:54