Zulip Chat Archive

Stream: new members

Topic: arithmetic proof with big constants


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

view this post on Zulip Simon Hudon (Apr 25 2019 at 01:14):

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

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

view this post on Zulip Travis Hance (Apr 25 2019 at 01:44):

That worked. Thank you!

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

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

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 04:46):

One of the questions on my undergraduate example sheets was: "which number is bigger: 21/20000000000002^{1/2000000000000} or 31/30000000000003^{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.

view this post on Zulip 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, g64g_{64} or BB(18)BB(18)? That's Graham's number vs the busy beaver function

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 05:48):

busy beaver hands down

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 05:48):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 05:48):

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

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 05:48):

Where does your intuition come from?

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 05:48):

Mine came from a children's book

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 05:49):

"Stinky Finger's House Of Fun"

view this post on Zulip Mario Carneiro (Apr 25 2019 at 05:49):

My intuition is BB is bigger than everything

view this post on Zulip Mario Carneiro (Apr 25 2019 at 05:49):

but I'm not sure about really small inputs

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 05:49):

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

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

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

view this post on Zulip Patrick Massot (Apr 25 2019 at 05:52):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 05:52):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 06:37):

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

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 06:38):

(which is of course much harder in binary)

view this post on Zulip Chris Hughes (Apr 25 2019 at 07:05):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:06):

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

view this post on Zulip Mario Carneiro (Apr 25 2019 at 07:09):

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

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

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:22):

Yes, sure it was. And yes, the point is that 23<322^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.

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 07:23):

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

view this post on Zulip Chris Hughes (Apr 25 2019 at 07:29):

Computer work is waaaay cheaper than human work.

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

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

view this post on Zulip 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=1012N=10^{12} and then rewrote for 2N and 3N and then never thought about the explicit value of N again

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

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