undone by powerful `refl` AI

Stream: maths

[Kevin Buzzard]

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.

[Simon Hudon]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

ha ha ha

[Kevin Buzzard]

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

[Kevin Buzzard]

the definition of 2000000000000 is 1000000000000 + 1000000000000

[Simon Hudon]

Riiiiight, yeah, that makes sense

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Simon Hudon]

I suggest you put this here in your Lean file:

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

[Floris van Doorn]

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

[Simon Hudon]

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

[Kevin Buzzard]

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?

[Floris van Doorn]

Yes, all of that makes sense and is correct.