Can we teach a computer to think about natural numbers the same way we do, that is, somehow non-axiomatically?
I’ve wondered about this as well. One possible way to go about this is to figure out how to introduce higher-order mathematical patterns into the process (instead of simply using atomic sentences and inference rules). Recurring proof patterns could be one such higher order pattern. Patterns at different scales could be compared, and new patterns suggested on the basis of this comparison. These new patterns could then be translated into a (or a number of) elementary propositions.
I’ve wondered about this as well. One possible way to go about this is to figure out how to introduce higher-order mathematical patterns into the process (instead of simply using atomic sentences and inference rules). Recurring proof patterns could be one such higher order pattern. Patterns at different scales could be compared, and new patterns suggested on the basis of this comparison. These new patterns could then be translated into a (or a number of) elementary propositions.