I think there is a difference here; the modern telescope doesn't output answers, claims or theorems - just data that still has to be interpreted to be even remotely useful.
It might superficially look like answers, but apparently someone still needs to interpret the results? Maybe it would be better to treat it like data.
they definitely do get answers. maybe the path is incomprehensible to you, but the yes or no answer is definitely there: that's what the formal provers are there for. In the worst case you have an Oracle which just answers your question with yes or no but in truth you get many more details if you want to look
Is it a correct answer, though? Even with a Lean proof, someone has to be verify that it proved the right theorem.
Checking that the theorem is what we really want to prove is much much less work than going through the whole proof though.
Oh, absolutely. Just saying there’s something for mathematicians to do before publishing results.