i'll use the first incompleteness theorem itself to explain this distinction between truth and proof
..the first because the second is essentially a stronger form of the first..
> First Incompleteness Theorem: "Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F." (o)
what's important is the statements are incapable of being proved or disproved, to me this is confusing language, let me try to show the possibilities
a statement can be:
o. proved : there exists at least one complete collection of validating evidence
i. disproved : there exists at least one complete collection of confuting evidence
ii. incapable of being proved : there only exists incomplete collections of validating evidence
iii. incapable of being disproved : there only exists incomplete collections of confuting evidence
..think of complete and incomplete in terms of russell's paradox(i): a set containing all sets; any proof would be incomplete because the evidence for the set containing all sets must also contain itself because it is a set; creating a subsequent requirement for evidence that this new self contained set is also contained in the set of all sets, ad infinitum, perpetually and subsequently incomplete..
the first incompleteness theorem is making a claim for the existence of ii and iii
if this statement is true how could you prove it?
if the statement is true it means you would need to prove that specific statements in the language of F are incapable of being proved or disproved, but if the statements themselves are incapably proved or disproved how can you express through evidence that your proof is even working on those same statements
a theorem is proved or disproved when one can express through finite steps, or statements of evidence, a proof
if a theorem has an incomplete proof or disproof how could i prove said incomplete proof?
but we know the statement to be true because that is how it essentially self references
by stating there are statements being incapably proved or disproved is itself incapable of being proved or disproved
making the statement true, but without proof of evidence
..except some strange brain itching intuition :P ..
but now we have left the domain of arithmetic and entered the domain of semantics(ii)
and here is where tarski comes in with his undefinability theorem{iii)
..is it irony that undefinability is underlined by this spell checker?..
coq is stating here that it is itself a semantic domain only dealing with arithmetic statements that can be proved or disproved
implying imperatively to avoid the incomplete and undefined because they explicitly and by design exist outside of this proof assistant's restricted domain of interest and so will be inexpressible
naively, if you wrote a program with the restriction of only computing the addition of positive integers; if you wanted to add using a negative integer you would have to write a new program
which going back to your original question:
> I've wondered how Gödel's incompleteness theorems come into play if Mathematicians are using proof assistants to verify their mathematics
they come into play only by being the very things that are disallowed in the spec from coming into play
in coq at least, you are required to work without them because it is written to only play with propositions that can be proved or disproved
and we showed above they are unable to be proved or disproved
(o) https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
(i) https://en.wikipedia.org/wiki/Russell%27s_paradox
(ii) https://en.wikipedia.org/wiki/Semantics
(iii) https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theo...