Be careful with the word "incomputable" (the article never said it was "undecidable" or "incomputable"); in computability theory BB(7910) is computable because

Be careful with the word "incomputable" (the article never said it was "undecidable" or "incomputable"); in computability theory BB(7910) is computable because it's just a single finite number. You could in theory specify a TM that writes down the answer without doing any calculation - incomputable problems necessarily involve unbounded outputs or inputs which prevents such trivial solutions. I realise you're talking about formal systems specifically (which corresponds to a some theorem-checking TM implementing that system) but when you allow any system of axioms (e.g. one with the value of BB(7910) of axioms) you basically ask whether any TM can compute that number (including one that already 'knows' it).