# Zulip Chat Archive

## 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

Let's solve that problem instead.

Last updated: May 14 2021 at 00:42 UTC