Zulip Chat Archive

Stream: maths

Topic: undone by powerful `refl` AI


view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:39):

I had just shown a classroom of children that 2 + 2 = 4 could be proved by refl and we got talking about the algorithm. I said it just simplified everything down to S(S(S(S(...)))=S(S(S(...))) and commented that it might well run out of memory if we try big numbers! So I tried

example : 1000000000000+1000000000000=2000000000000 := by refl

and it typechecked! I was like "wooah kids, someone has updated the refl AI! I never knew it did that!" When did refl know about column addition? I know that @Floris van Doorn laughed once when I told him that refl was an AI.

view this post on Zulip Simon Hudon (Sep 23 2019 at 19:45):

What if you run that file with lean --trust=0. I'm wondering if it's sped up by using a macro

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:53):

oh rofl I think I see what's happening :-)

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:53):

ha ha ha

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:54):

example : 1000000000000+2000000000000=3000000000000 :=  by refl -- deterministic timeout

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:54):

the definition of 2000000000000 is 1000000000000 + 1000000000000

view this post on Zulip Simon Hudon (Sep 23 2019 at 19:57):

Riiiiight, yeah, that makes sense

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:58):

I guess that is not obvious. Am I right? Where is the algorithm which turns strings of digits into a nat?

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 19:59):

Do you think it does the divisions etc in base 10 using long division?

view this post on Zulip Simon Hudon (Sep 23 2019 at 20:00):

I suggest you put this here in your Lean file:

set_option pp.numerals false
#check 1000000000000+2000000000000=3000000000000

view this post on Zulip Floris van Doorn (Sep 23 2019 at 20:01):

Numerals are turned into a binary representation (using the auxiliary functions bit0 and bit1).

view this post on Zulip Simon Hudon (Sep 23 2019 at 20:02):

What happens is that those digits turn into a term where we're using bit0, bit1 and one (the functions) to represent the same numbers in binary

view this post on Zulip Kevin Buzzard (Sep 23 2019 at 20:29):

Does some part of the parser just completely unfold every string-of-digits-representing-a-nat completely into a bit0 bit1 bit0 ... representation before any other part of the system can get to it? I guess that's how it works. Then yeah definitely 2000000000000=1000000000000+1000000000000 is easy, the head terms are has_add.add and bit0 and then bit0 unfolds to has_add.add and it's all over -- the terms are now syntactically equal. Am I making sense?

view this post on Zulip Floris van Doorn (Sep 23 2019 at 20:39):

Yes, all of that makes sense and is correct.


Last updated: May 10 2021 at 07:15 UTC