metamath natural number game

Stream: general

[Kevin Buzzard]

https://github.com/pbrosnan/ntg

With added proof that 0 = 1?? I never managed to do that level in Lean...

[Reid Barton]

Ah yes the "invulnerability" upgrade

[Adam Topaz]

Reid Barton said:

Ah yes the "invulnerability" upgrade

is that like god-mode in doom?

[Jason Rute]

pa_ax7 is OP

[Eric Rodriguez]

New ZF patch dropped! Adds new game-mode "choice"

[Mario Carneiro]

For some context: The metamath peano.mm file has never been used, it is an axiomatization written in a very obtuse form for theoretical analysis purposes. The typo has already been fixed, although the PR hasn't landed yet. It won't cause any breakage because there are no proofs in the system (except for this ntg repo, apparently)

[Kevin Buzzard]

Is my understanding correct that this typo was made by the famous set-theorist Bob Solovay?

[Mario Carneiro]

The very same

[Mario Carneiro]

It's understandable, because the way in which the statement was wrong has to do with the difference between FOL and metamath: specifically, you have to say that a binder variable is fresh with respect to the variables occurring in the formula, which is true by default in FOL and false by default in metamath

[Mario Carneiro]

We actually have a tool which runs on set.mm that would have caught this bug, but it is adapted specifically to set.mm and other databases that look vaguely like it, while peano.mm has a very different design

[Mario Carneiro]

In short, bob thought he wrote this:

axiom lt_def (x y : ℕ) : x < y ↔ ∃ z, y = x + nat.succ z

but he actually wrote this:

axiom lt_def' (x y : ℕ → ℕ) (z : ℕ) : x z < y z ↔ ∃ z, y z = x z + nat.succ z

which is false:

example : false :=
begin
  obtain ⟨z, h⟩ := (lt_def' (λ z, 0) (λ z, z) 1).1 dec_trivial,
  simpa [nat.succ_eq_add_one] using h,
end

[Jason Rute]

It should be noted that Bob Solovay also found one of the two inconsistencies in the HOL Light theorem prover kernel (the other being found by Tom Hales). These were fixed of course and John Harrison later gave a HOL Light proof of the consistency of the HOL Light kernel. So I think in the end, Solovay’s impact on the consistency of theorem provers is probably a net positive. (Note, this story comes from my memory of what @Jeremy Avigad told me. I can’t find it documented.)

[Kevin Buzzard]

I have a huge amount of respect for Solovay as a mathematician, and this is in no way lessened by a typo. Every mathematician has a typo in their papers.

[Jeremy Avigad]

It would be good to document this. I think I first heard the story from Tom Hales, and my memory is that the bug had to do with variable renaming. (The companion story is that when I was a graduate student at Berkeley, my advisor, Jack Silver, decided to teach a course on proof theory, and Bob Solovay decided to sit in. In the first lecture, Jack said something about renaming variables, and Bob pushed him on the details. Jack got flummoxed, came back the next lecture, and offered a correction. Bob challenged that and found another bug in the presentation. Jack gave up, moved on, and Bob did not come back for the third lecture.)

Bob and Tom and I all attended a meeting at Dagstuhl in the early days of Flyspeck. Between the talks Bob tried to sort out the set-theoretic strength of Coq's axiomatic foundation, which is essentially the same as Lean. (It has long been folklore that these have the same strength as set theory with omega-many inaccessibles; the most rigorous proof I know of the lower bound is Mario's formalization of set theory in Lean, and the most rigorous proof I know of the upper bound is Mario's MS thesis.) Tobias Nipkow was at the meeting; it is when he got involved with Flyspeck. Freek Wiedijk was also there, and if I recall correctly it was the first time I met Assia Mahboubi.

Oh! And now I remember that it was this meeting of the MAP group: https://www.dagstuhl.de/de/programm/kalender/semhp/?semnr=05021. I had recently completed the formalization of the prime number theorem, Georges had just announced the formalization of the four-color theorem (he was not at the meeting), and Tom had not quite finished the formalization of the Jordan curve theorem. Harold Edwards was also there, talking about the Edwards curve. Edwards has done excellent work on the history of 19th century number theory (he is a big fan of Kronecker), and I gave him a draft of a paper I had written on Dedekind for comments. When the lectures got too technical, sitting in the back of the lecture room, I watched him pull out the paper, scowl at my comparisons between Dedekind and Kronecker, and fill the margins with notes (which we later discussed).

Thanks for the trip down memory lane! Anyhow, someone should document the story of the bugs in HOL light. Tom and John Harrison are more reliable sources than I am.