search

leanprover-community / NNG4

Natural Number Game
https://adam.math.hhu.de
Apache License 2.0
111 stars 34 forks source link

Strong induction world #10

Open kbuzzard opened 1 year ago

kbuzzard commented 1 year ago

I have a strong induction world in the lean 3 version of NNG but I never got around to putting it online. It's here. This needs to be broken up into bite-sized pieces, translated into Lean 4, and added as a new world.

ndcroos commented 3 months ago

Hi, I'd like to work on this issue. Can this be assigned it to me please?

kbuzzard commented 2 months ago

Sure!

For reviewing purposes, can you start by just adding a few levels? It seems to me that some of the levels I suggest in the route above are already in NNG4, or should not be in strong induction world. So some design decisions need to be made here. One possibility is that you start with a proof of strong induction and work back to see exactly which facts you need about <, and then basically make a new world which is basically < world with a proof of strong induction at the end.