There is some of this in incredible.pm, and there's some of it in NNG. I made very little use of previous results in either one, except for a few levels of NNG that shame you for not generating simple proofs from immediately previous results.

incredible.pm's "gameplay" element where you're challenged to prove the theorem in as few statements (blocks) as possible works against the idea of developing a bank of theorems and then applying those theorems to prove other theorems. I'm not so fond of it.

> (b) I much prefer the textual input —even with the "guess the verb" problem— to clicking and dragging wires and blocks

That's fair. The bigger issue I have is that in incredible.pm you're free to make statements if you think those statements will be useful to you, while NNG is very strict about making you work with only the statements you're given.

In fact, there is one level in incredible.pm where I solved it in what was listed as the minimum number of blocks, but one of those blocks was a label. The label block is not doing any logical work, but sure enough, if I deleted the label block, incredible.pm was unable to unify the output that I had routed into the label block with the input that I had routed the label block into. So it would appear that at least one of the levels in incredible.pm specifically expects you to introduce your own statement with your own phrasing as an aid.

> (c) I feel like I've learned something about how to use Lean, while it seems unlikely I'd be able to transfer much from the UX of incredible.pm

I should be fair to NNG: I had extreme difficulty using existential statements correctly in incredible.pm, and more moderate difficulty managing to correctly use universal generalization. I think solving those levels gave me at least a decent mental model of how the theorem prover was handling quantifiers internally, and that should have transferred to a textual interface -- although it hasn't really stuck in my mind.

> the old, Lean 3, NNG had as its crux "trichotomy for ℕ"; that was very satisfying to finally prove!

That's still present in the current NNG. It is the proof I spent so much time complaining about above, the final level of Inequality World. (Or rather, that level wants you to prove that any two natural numbers are comparable, but you must use the trichotomy in order to do that, and you can't use what you haven't proved.)

--------

I think NNG would benefit a lot from including more difficult proofs. (And from letting you introduce your own intermediate goals!) I was proud when I finished the proof that ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x))) . I had to think about what the theorem was saying and write down a plan of attack. NNG doesn't really have anything like that.

--------

Something I really did like in NNG was the remarks about (and eventual proof of) injectivity of the successor function. It's very interesting to me that the proof is based on, as NNG describes it, "the mathematically pathological pred[ecessor] function" - but only on cases where the pathology doesn't exist. (The proof involved introducing the function, making it inaccessible to the player, and instead giving the player the theorem "pred succ n = n", which is true without any exceptions.)

Cool; it wasn't there yet 6 weeks ago: https://news.ycombinator.com/item?id=37880788

"pred succ n = n" reminds me a lot of def'ns of the form "(left p, right p) = p"; I'll have to think about that a bit. Injectivity of succ is, I guess, what distinguishes ℕ from similar constructions with different characteristic? (did I just think that, or am I parroting NNG?)

> ∀x.(r(x)→⊥)→r(f(x)) ⟹ ∃x.r(x)∧r(f(f(x)))

I think I gave up on incredible.pm too early (although I did skip ahead for SKI) ... I'll have to go back and try that. It seems to have a bit of the flavour of "all people who claim to be Sir Anthony Charles Lynton Blair KG are liars"

NNG gives you the pred_succ theorem, and calls it a theorem, but I don't see how it's supposed to be proved. Suppose the successor to 9 were 3. What's stopping that from being the case?

I don't see that pred_succ ("pred succ n = n" for all n) is a lemma from which succ_inj can be proved - it looks to me like pred_succ is logically equivalent to succ_inj. Each is true if and only if the other is.

Here the problem is not so much that the pred function is mathematically pathological as that the axioms, without the axiom that the successor function is injective, do not allow us to define a predecessor function at all. The guarantee that when, you call succ on nine, you don't get a number that is also the successor of some other number -- which is necessary in order for pred_succ to be a valid theorem -- is precisely the statement that succ is injective.

Am I missing something?

I was very wrong earlier: characteristic is taken care of by 0 not being a successor; injectivity of succ also allows circular pseudo-nats.

PS. found Peano (1889): https://archive.org/details/arithmeticespri00peangoog/page/n...

  his:
  7.  a,b ∈ N .Ↄ: a = b .=. a+1 = b+1
  8.  a ∈ N .Ↄ. a+1 -= 1
  are our:
  7.  a,b ∈ ℕ ⇒ (a = b ↔ S a = S b)
  8.  a ∈ ℕ ⇒ S a ≠ 0

This is prevented by saying that the successor function is a function. If a = b, then S(a) necessarily equals S(b). (The other half of axiom 7, the statement that when S(a) = S(b) then a = b, is the definition of an injective function. It's what prevents us from saying that the successor to 9 is 3.)

There is a fun image of dominos on the wikipedia page for the Peano axioms that explains how the structure of the natural numbers is constrained by the axioms.

A backwards loop from a number in the chain of succession from zero to an earlier number in the same chain can't happen because the successor function is injective.

A backwards fork (two chains meeting) can't happen for the same reason.

A forwards fork would be invisible to us as long as our only available tool is the successor function, which will always choose the same branch of the fork. This essentially means that forwards forks don't exist. There could be a larger structure in which it is true that e.g. the "9" node has one outgoing edge pointing to "10" and another one pointing to "green", but only one of those edges can be the edge picked out by the successor function, so our structure would only include one of the "10" or "green" nodes.

A loop parallel to the chain of succession from zero [imagine the normal chain "0, 1, 2, ..." alongside the three special elements 甲 乙 丙 arranged in a three-element circle] is ruled out by axiom 9, which says that any set that contains the chain of succession from zero contains all the natural numbers.

thinking out loud...

we are free to define a predecessor function by saying it is the inverse of the successor function. That definition would immediately prove the pred_succ theorem, as long as the successor function is invertible. Half the definition of being invertible is being injective, so this doesn't let us prove succ_inj in a non-circular way.

I don't know how else we would attempt to define the predecessor function, given the algebraic structure we're working with where all values take the form "0" or "succ n".

  induction y with d hd
  right
  apply zero_le
  cases hd with hdl hdr
  left
  cases hdl with e he
  use succ e
  rw [add_succ,he]
  rfl
  cases hdr with w hw
  cases w with z nz
  left
  use 1
  rw [hw]
  tauto
  right
  rw [hw,add_succ,← succ_add]
  use z
  rfl