## Stream: new members

### Topic: arithmetic proof with big constants

#### Travis Hance (Apr 25 2019 at 00:31):

I want to prove a simple arithmetic calculation theorem:

theorem x : 9000 / 3 = 3000 := rfl


This works for smaller numbers, but for the given example, I get a warning about "(deterministic timeout)". How exactly does the arithmetic scale? What's the suggested way to deal with things like this?

I notice that #eval isn't absurdly slow or anything, e.g.,

#eval 90000000000 / 3


works fine. So how come when constructing proof terms it chokes on such small numbers?

#### Simon Hudon (Apr 25 2019 at 01:14):

try import tactic.norm_num and by norm_num (from mathlib)

#### Simon Hudon (Apr 25 2019 at 01:17):

#eval uses the virtual machine to do its computation. In the virtual machine, natural numbers are implemented very efficiently: it uses libgmp. With rfl, the computation is done using logical reduction rules the definition of nat in the logic is very inefficient: it uses unary representation.

#### Travis Hance (Apr 25 2019 at 01:44):

That worked. Thank you!

#### Travis Hance (Apr 25 2019 at 01:46):

I see the proof term it generates is doing some binary representation thing. That's pretty neat.

#### Simon Hudon (Apr 25 2019 at 01:49):

Yes, that's the cool thing about numerals. the lexeme 10  is syntactic sugar for bit0 (bit1 (bit0 one)) which are functions that evaluate into succ and zero (in the case of nat) but which don't have to be evaluated to do arithmetic.

#### Kevin Buzzard (Apr 25 2019 at 04:46):

One of the questions on my undergraduate example sheets was: "which number is bigger: $2^{1/2000000000000}$ or $3^{1/3000000000000}$?" I had to be careful when formalising the result in Lean. In theory I could work out both sides to 20 decimal places and I'd be done, but Lean cannot do this yet with a verified argument (as far as I know) so I had to use other tricks.

#### Mario Carneiro (Apr 25 2019 at 05:47):

Oh, this reminds me of a recent question that came up on puzzling.SE: Which is bigger, $g_{64}$ or $BB(18)$? That's Graham's number vs the busy beaver function

#### Kevin Buzzard (Apr 25 2019 at 05:48):

busy beaver hands down

#### Kevin Buzzard (Apr 25 2019 at 05:48):

even BB(12) is bigger than Graham's number, right?

#### Mario Carneiro (Apr 25 2019 at 05:48):

that's my intuition as well, but I have no idea how to prove it

#### Kevin Buzzard (Apr 25 2019 at 05:48):

Where does your intuition come from?

#### Kevin Buzzard (Apr 25 2019 at 05:48):

Mine came from a children's book

#### Kevin Buzzard (Apr 25 2019 at 05:49):

"Stinky Finger's House Of Fun"

#### Mario Carneiro (Apr 25 2019 at 05:49):

My intuition is BB is bigger than everything

#### Mario Carneiro (Apr 25 2019 at 05:49):

but I'm not sure about really small inputs

#### Kevin Buzzard (Apr 25 2019 at 05:49):

One of the characters in it. Brian Brain, at some point makes exactly the same observation

#### Kevin Buzzard (Apr 25 2019 at 05:49):

"all of these are dwarfed by Busy Beaver 12", he says. I had to go to Wikipedia to look up the Busy Beaver function

#### Mario Carneiro (Apr 25 2019 at 05:51):

wikipedia actually contains a statement that BB(12) is bigger than 3^^^^3, but it doesn't say about g64

#### Patrick Massot (Apr 25 2019 at 05:52):

BB(8) is not so tall, especially when standing on sand

#### Mario Carneiro (Apr 25 2019 at 05:52):

Oh, it also mentions that BB(17) > g64

#### Mario Carneiro (Apr 25 2019 at 06:37):

Your question about $2^{1/2000000000000}<3^{1/3000000000000}$ boils down to proving $\log_23<3/2$, or $2^3<3^2$; I don't think any high precision estimates are needed

#### Mario Carneiro (Apr 25 2019 at 06:38):

In fact the hardest part, numerically, is just showing that 2000000000000 = 2 * 1000000000000 and 3000000000000 = 3 * 1000000000000

#### Mario Carneiro (Apr 25 2019 at 06:38):

(which is of course much harder in binary)

#### Chris Hughes (Apr 25 2019 at 07:05):

But it would require no work if we could do high precision estimates.

#### Mario Carneiro (Apr 25 2019 at 07:06):

It would require a lot of work, by the computer. Nothing is free

#### Mario Carneiro (Apr 25 2019 at 07:09):

If you prove (x + 1)^100 = (1 + x)^100 by using ring, I will be sad

#### Mario Carneiro (Apr 25 2019 at 07:11):

I'm pretty sure that question was written specifically to foil attempts to prove it by plug-and-chug calculator methods

#### Kevin Buzzard (Apr 25 2019 at 07:22):

Yes, sure it was. And yes, the point is that $2^3<3^2$, but it was interesting to prove this in Lean because you had to be careful to never write anything which triggered a computation.

#### Kevin Buzzard (Apr 25 2019 at 07:23):

I proved some general lemma first, and then applied it to get the result.

#### Chris Hughes (Apr 25 2019 at 07:29):

Computer work is waaaay cheaper than human work.

#### Mario Carneiro (Apr 25 2019 at 07:39):

the computer will be asked to solve this problem many many times on many many computers though. Think of the environment

#### Mario Carneiro (Apr 25 2019 at 07:39):

also if you ever want to move this proof anywhere else, it helps if you didn't write intentionally bad proofs

#### Kevin Buzzard (Apr 25 2019 at 07:40):

In fact the hardest part, numerically, is just showing that 2000000000000 = 2 * 1000000000000 and 3000000000000 = 3 * 1000000000000

My memory is that this is exactly where I started: I set $N=10^{12}$ and then rewrote for 2N and 3N and then never thought about the explicit value of N again

#### Kevin Buzzard (Apr 25 2019 at 07:40):

I would dig it out from the xena archives but I'm busy wrestling with type class hell

#### Chris Hughes (Apr 25 2019 at 07:41):

the computer will be asked to solve this problem many many times on many many computers though. Think of the environment