This shows why it DOES matter: Both Collatz and p² = 2q² require going above arithmetic to even state them (“for ALL numbers...”). That’s the key insight—we can’t even formulate these interesting conjectures within pure arithmetic, let alone prove them. In pure arithmetic we can only check specific cases:
“4 goes to 2”
“3² ≠ 2×2²”
The theorem prover point is interesting but misses the key distinction:
Yes, theorem provers operate at a mechanical/syntactic level
But they still encode and use higher mathematical concepts
The proofs they verify still require going above pure arithmetic
The mechanical verification is different from staying within arithmetic concepts
In pure arithmetic we can only:
Do basic operations (+,-,×,÷)
Check specific cases
Compute results
Any examples of real conjectures proven while staying at this basic level?