prime number world

[kbuzzard]

This would depend on divisibility world, and my vision of the goal is a proof that 2 is prime.

Following mathlib we could define p to be IsPreprime if a | p -> a = 1 \or a = p. Note that the difference between IsPreprime and IsPrime is that 1 is Preprime; the definition of prime would be 2 <= p \and IsPreprime p.

One design decision needed here: whether to let the user have access to mathlib's interval_cases tactic. FThis will turn a goal of P(k) plus a hypothesis k <= 2 to the three goals P(0), P(1) and P(2). For now I say no.

My vision is: make the user prove manually that k<=2 implies k=0 or k=1 or k=2 (which we've done in <= world; probably this lemma should be moved to this world; note however that we use k<=1 implies k=0 or k=1 in advanced multiplication world so we can't move that) and then that 2 is prime using the fact that a | 2 => a <= 2 (which we need to do in divisibility world; we will prove there that a | b and b != 0 => a <= b).

Perhaps we should also have a definition of preprime like in mathlib: IsPreprime n means a | n => a = 1 or a = n (so 1 is preprime and not prime). Note to self: have we taught the user how to deal with \and hypotheses and goals? No! So need to explain this with cases.

[ftm-2005]

Hello, is there a list of suggested levels for Prime World? A partner and I just finished proving the following levels for a potential division world and plan to use them for Prime world as suggested:

1. 1 | n
2. n | n
3. n | 0
4. If a | 1 then a = 1
5. if a | b and b | c then a | c
6. If 0 | n then n = 0
7. if a | b and b != 0 then a <= b
8. if a | b and b | a then a = b
9. if a | b and a | c then a | b + c
10. If a | b then a | b * c
11. if a | b then a * c | b * c
12. if a | b and a ≠ b then ¬ (b ∣ a)

[kbuzzard]

In mathlib they have the funkier statement "if a | b then (a | c <-> a | (b + c))", but this discussion really belongs in the divisibility world issue. Sorry, I have a big talk to worry about next week and i've not been looking at github notifications at all. I will come back to all this on 14th June.

[coolujain]

Hello, me and my partner attempted to prove that 2 is prime and realized that the theorems done in other worlds (assuming the division world levels my partner listed above exist) are enough to do that proof. However, our proof used constructer which we are not sure if we are allowed to introduce in the game or not. Moreover, we approached the proof in two ways:
1 - The goal would be "prime 2" the user would then have to use unfold prime to proceed with the proof. (This way requires introducing both constructer and unfold)
2- The goal would be " (2 ≤ 2) ∧ ( m ∣ 2 → m = 1 ∨ m = 2) ". (This way requires only introducing constructer)
Please let us know what way would be more suitable for the game or if there's an alternate way we should try.

[coolujain]

Hello, me and my partner @ftm-2005 created a prime world with 5 levels:
Level 1 : Prove that 1 is not prime
Level 2 : Prove that 2 is prime
Level 3 : Prove that if p is prime and q is prime and p | q then p = q
Level 4 : Prove that 4 is not prime
Level 5 : Prove that the product of two primes is not prime (boss level)

Notes :

• We used the tactic constructor in most the levels to split and statements.
• For each one of these levels we've done a version using unfold (to unfold the definition of prime) and a version not using unfold because we aren't sure if that's a tactic you would like to introduce in the game.
• We ran into an issue in level 4 where the number 2 is not recognized as a natural number (we used succ 1 instead).
• We suggest to add simp_dvd to check if a number divides another. For example 2|4 should be true.
  -When the goal is false and we have a hypothesis that says 2 <= 1, currently a lot of tactics need to be applied to solve the goal. However, it got a little repetitive and we suggest allowing simp to close that goal as that currently works in lean outside of NNG.
• Our prime world depends on the division world that we created and sent a pull request for , hence we will not be making a pull request for prime world until our division world is confirmed but here is the link to the fork which contains prime world.
  https://github.com/coolujain/NumbersGame2.git