I am having a go at creating a program that does math like a human. By inventing statements, assigning probabilities to statements (to come back and think more deeply about later). But I'm stuck at the first hurdle.
If it is given the proposition
So, like a human it might test this proposition for a hundred or so numbers and then assign this proposition as "unlikely to be true". In other words it has concluded that all natural numbers are not equal to 123. Clearly ludicrous!
On the other hand this statement it decides is probably false which is good:
∃x∈ℕ: x+3 ≠ 3+x
Any ideas how to get round this hurdle? How does a human "know" for example that all natural numbers are different from the number 456. What makes these two cases different?
I don't want to give it too many axioms. I want it to find out things for itself.