Sharing my first day experience

Stream: new members

[Weiyi Wang]

Me: all right, let me try with some little theorem I had in high school. Here it goes, "Let {a_n} be the sequence by sorting all numbers like sℕ + tℕ for some constants s and t..."
Lean: hold on. Is that even well defined?
Me: well obviously... bullshitting my way through with 200+ lines of random theorems and tactics for a whole day... there, you happy?

This is weirdly fun.

[Kevin Buzzard]

My first day was "let's prove that the statement $x^2-3x+2=0 \implies x=1$ is false. My proof: "$x=2$ duh". Lean's response "OK so now you've got to prove two things not one: firstly $x^2-3\times 2+2=0$ and secondly $2\not=1$ (and this was in 2017 before norm_num and ring...)

[Julian Berman]

Did you have to walk uphill both ways then?

[Kevin Buzzard]

No I just had to bug Mario to PR norm_num :-) (oh actually it looks like Simon Hudon did it? https://github.com/leanprover-community/mathlib3/pull/17 . Here is the history of $2^2-3\times 2+2=0$ and the birth of norm_num: https://github.com/leanprover-community/mathlib3/issues/16

[Kevin Buzzard]

-- example : (5:real) ≠ 8 := by norm_num  -- excessive memory consumption
-- example : (10:real) > 7 := by norm_num -- (deterministic) timeout

:-)

[Mario Carneiro]

Kevin Buzzard said:

No I just had to bug Mario to PR norm_num :-) (oh actually it looks like Simon Hudon did it? https://github.com/leanprover-community/mathlib3/pull/17 . Here is the history of $2^2-3\times 2+2=0$ and the birth of norm_num: https://github.com/leanprover-community/mathlib3/issues/16

I definitely remember writing norm_num, but based on the history I think what happened is that Simon wrote a version of norm_num based on reflection, probably in response to a discussion involving you, and I liked the idea but not the execution and rewrote it in the subsequent commit

[Mario Carneiro]

and of course before both Simon and I worked on it there was a version of norm_num in lean core written by Leo which had no user-facing syntax and I think was used in some eblast internals or something

[Kevin Buzzard]

IIRC it was "mostly there but not a user-facing tactic" at the point where I started whingeing about it, i.e. there was nothing in tactic.interactive?

[Mario Carneiro]

right

[Mario Carneiro]

although I think the version I wrote ended up independent of tactic.norm_num because that one only supported addition and multiplication and I wanted other operations as well

[Mario Carneiro]

it was rewritten again a while after that to support norm_num extensions, and then once more in the move to lean 4 and I think that's the current version