4 ms·
You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if
by lisper 2y ago
You'd be surprised at the number of things that appear to be self-evidently true that turn out to depend on tacit assumptions. For example, is 7 prime? Not if you're doing modular arithmetic.
- sebzim4500 2y agoIt's a joke about `i` being imaginary.
- fat_cantor 2y agoyes the joke is on i
- lohfu 2y agoi think they were joking, but i can't prove it
- mathgradthrow 2y agoIt's also independently pretty tedious to explain that 7 is prime to a proof checker.
- amenghra 2y agoIs it? You can tell the checker about the remainder of division by 2 to 6.
- deleted 2y ago[deleted]
- kevhito 2y agoMaybe also need to show that there are no other naturals between 1 and 7? And also that numbers greater than 7 can't be a divisor of 7?
- someplaceguy 2y agoThe first one can be trivially proved with automatic decision procedures and the second one is also very easy to prove, I believe.
- drhodes 2y agoThe proof is not too bad in Lean4. I'm nothing special and I've got it down to 9 lines. But, maybe that is considered pretty tedious vs. what expectations one might have. In any case, it is an exercise in Heather MacBeth's free book: The Mechanics of Proof, https://hrmacbeth.github.io/math2001/04_Proofs_with_Structure_II.html#id32 https://hrmacbeth.github.io/math2001/04_Proofs_with_Structur... btw, that book is a lot of fun to work through.
- mathgradthrow 2y agoThe obvious proof term for isprime p is exponential compared to the size of p. The AKS proof term is polynomial, but still very bad.
- mathgradthrow 2y agohttps://en.m.wikipedia.org/wiki/Primality_certificate https://en.m.wikipedia.org/wiki/Primality_certificate
- deleted 2y ago[deleted]