> (a) the sequence felt more like actual theory* building than figuring a few cool puzzles
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.)