This is a special post for quick takes by Nicolas Macé. Only they can create top-level comments. Comments here also appear on the Quick Takes page and All Posts page.
Here's one of the math facts I find the hardest to wrap my head around: There are some finite, well-defined integers that are impossible to compute within PA or ZF.
The argument goes roughly like this: We'll define a finite integer that is such that computing would be equivalent to proving ZF's consistency. Then we're done because by an incompleteness theorem, ZF cannot prove its own consistency. So how to construct such a number? First construct a Turing machine that halts (on a blank tape) iff ZF is inconsistent. Say it has states. The busy beaver number is defined as the maximal number of steps a Turing machine with states takes when ran (on a blank tape), assuming that it halts. If we knew we'd need to run our TM at most steps to prove ZF's consistency. So we've constructed an that's as claimed.
One observation that dissolves a little bit of the mystery for me: We can devise, within ZF, a set of properties that points to a unique integer . We can write down this integer, of course, but ZF won't be able to notice that it's the one that we're after, because if it did it'd prove its own consistency.
Things like this are not quite "particular integers" though in the informal sense (19 is centrally a "particular integer", BB(1000) isn't). They are more like integer-definitions whose meaning (as particular integers) can't be characterized in some ways.
Similarly, the decision that an agent will eventually make is not a "particular decision" from the point of view of that agent, but a decision-definition whose meaning as a particular decision that agent can't yet divine, because it's not yet decided. Some external oracle might know more about the meaning of the decision-definition and predict what the decision will be before the agent makes the decision. And a stronger theory might "know" (in a given sense) which particular integer an integer-definition formulated in a weaker theory designates, or at least have some better characterization of it available.