Can the AI recognize such situations and say "no way, this formal system doesn't seem to describe my regular integers"?

It need not -- asking whether a formal system "describes my regular integers" is a disguised query for whether it satisfies some set of properties that happen to be useful. All the AI needs to be able to do is evaluate how effectively different models describe whatever it's trying to use them to describe.

Unfortunately, if we have an arithmetical statement that we can neither prove or disprove so far, your idea would have us believe that it's true and its negation is also true. That doesn't look like correct Bayesian reasoning to me!

I don't see why not. It's not that we would believe the statement and its negation are both true; rather, we would believe that the statement is true with probability x and false with probability 1-x, as usual.

cousin_it:

For example, we can add to PA some axiom that rules out its standard model, but leaves many nonstandard ones. The simplest example would be to add the inconsistency of PA - the resulting theory will (counterintuitively) be just as consistent as PA, but quite weird. [...] Can the AI recognize such situations and say "no way, this formal system doesn't seem to describe my regular integers"?

This seems to be a matter of some relatively straightforward human heuristics. A theory that is somehow directly "talking about itself" via its axioms looks weird and suspicious. And not to mention what this axiom would look like if you actually wrote it down alongside the standard PA axioms in the same format!

Note that when these heuristics don't apply, humans end up confused and in disagreement about what should be considered as "our regular" stuff when faced with various independent statements that look like potential axioms. (As with Euclid's fifth postulate, the continuum hypothesis, the axiom of choice, etc.)

It will have many interesting provable theorems that are nevertheless common-sensically "false", e.g. "PA proves 1+1=3".

More specifically, it will prove: "There exists a natural number that, when decoded according to your Goedelization scheme, yields a proof in PA that 1+1=3." However, it won't prove anything about that number that would actually allow you to write it down and see what that proof is. ("Writing down" a natural number essentially means expressing a theorem about a specific relation it has with another number that you use as the number system base.) This suggests another straightforward heuristic: if the theory asserts the existence of objects with interesting properties about which it refuses to say anything more that would enable us to study them, it's not "our regular" kind of thing.