## Stream: general

### Topic: Graham's number

#### Mario Carneiro (Oct 25 2019 at 22:31):

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 (Oct 25 2019 at 22:32):

no one ever talks about the 0 base case

#### Kevin Buzzard (Oct 25 2019 at 22:34):

wait, this times out on my my machine

#### Mario Carneiro (Oct 25 2019 at 22:34):

I would be very impressed if it didn't

#### Kevin Buzzard (Oct 25 2019 at 22:35):

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

#### Mario Carneiro (Oct 25 2019 at 22:35):

just wait for moore's law to catch up

#### Kevin Buzzard (Oct 25 2019 at 22:36):

or for the sun to burn out

#### Mario Carneiro (Oct 25 2019 at 22:38):

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

#### Mario Carneiro (Oct 25 2019 at 22:39):

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

#### Kevin Buzzard (Oct 25 2019 at 22:40):

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

#eval f^[4] 6 -- 10


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

it's in core

oh wow

#### Mario Carneiro (Oct 25 2019 at 22:41):

nat.iterate

#### Kevin Buzzard (Oct 25 2019 at 22:41):

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

#### Kevin Buzzard (Oct 25 2019 at 22:41):

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

#### Mario Carneiro (Oct 25 2019 at 22:41):

No, I think it is

#### Mario Carneiro (Oct 25 2019 at 22:42):

it's not computable though :P

#### Mario Carneiro (Oct 25 2019 at 22:42):

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

#### Mario Carneiro (Oct 25 2019 at 22:43):

I think TREE(3) is provable and computable

Last updated: Dec 20 2023 at 11:08 UTC