Zulip Chat Archive

Stream: general

Topic: Graham's number


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:32):

no one ever talks about the 0 base case

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 22:34):

wait, this times out on my my machine

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:34):

I would be very impressed if it didn't

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 22:35):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:35):

just wait for moore's law to catch up

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 22:36):

or for the sun to burn out

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:38):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:39):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:41):

it's in core

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 22:41):

oh wow

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:41):

nat.iterate

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 22:41):

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

view this post on Zulip Kevin Buzzard (Oct 25 2019 at 22:41):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:41):

No, I think it is

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:42):

it's not computable though :P

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:42):

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

view this post on Zulip Mario Carneiro (Oct 25 2019 at 22:43):

I think TREE(3) is provable and computable


Last updated: May 08 2021 at 17:33 UTC