Graham's number

Stream: general

[Mario Carneiro]

Inspired by a recent numberphile video, here's Graham's number in lean:

-- knuth e m n = m ^(e) n
def knuth : ℕ → ℕ → ℕ → ℕ
| 0     m n := m * n
| (e+1) m n := (knuth e m)^[n-1] m

def g : ℕ → ℕ
| 0 := 4
| (n+1) := knuth (g n) 3 3

def graham_number := g 64

#eval graham_number

[Mario Carneiro]

no one ever talks about the 0 base case

[Kevin Buzzard]

wait, this times out on my my machine

[Mario Carneiro]

I would be very impressed if it didn't

[Kevin Buzzard]

my machine would need a lot more atoms than the universe could provide, I suspect

[Mario Carneiro]

just wait for moore's law to catch up

[Kevin Buzzard]

or for the sun to burn out

[Mario Carneiro]

I guess TREE(3) is probably impossible to define in lean

[Mario Carneiro]

oh actually I take that back, you only need second order arithmetic to prove it exists

[Kevin Buzzard]

def f : ℕ → ℕ := λ x, x + 1

#eval f^[4] 6 -- 10

Since when has that been a thing? I didn't know about that thing

[Mario Carneiro]

it's in core

[Kevin Buzzard]

oh wow

[Mario Carneiro]

nat.iterate

[Kevin Buzzard]

Is that busy beaver number which is unknowable definable in Lean? I guess not.

[Kevin Buzzard]

https://www.scottaaronson.com/blog/?p=2725

[Mario Carneiro]

No, I think it is

[Mario Carneiro]

it's not computable though :P

[Mario Carneiro]

It's actually within our capabilities given the computability theory stuff

[Mario Carneiro]

I think TREE(3) is provable and computable