Yes, you absolutely can argue computer verified proofs. They are very likely to be true (same as truth in biology or sociology: a social construct), but to be certain, you would need to solve the halting problem to proof the program and it’s compiler, which is impossible. Proofing incompleteness with computers isn’t relevant, because it wasn’t in question and it doesn’t do away with it’s epistemological implications.
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that C++ is Turing complete does not prevent programs created from it from verifying the proofs that they have verified. The proof of the halting problem (and incompleteness proofs based on the halting problem) itself halts. https://leanprover-community.github.io/mathlib_docs/computability/halting.html
I explicitly refer to your second paragraph.
Yes, you absolutely can argue computer verified proofs. They are very likely to be true (same as truth in biology or sociology: a social construct), but to be certain, you would need to solve the halting problem to proof the program and it’s compiler, which is impossible. Proofing incompleteness with computers isn’t relevant, because it wasn’t in question and it doesn’t do away with it’s epistemological implications.
It is not necessary to solve the halting problem to show that a particular lean proof is correct.
Lean runs on C++. C++ is a turning complete, compiled language. It and it’s compiler are subject to the halting problem.
The fact that C++ is Turing complete does not prevent it from computing that 1+1=2. Similarly, the fact that C++ is Turing complete does not prevent programs created from it from verifying the proofs that they have verified. The proof of the halting problem (and incompleteness proofs based on the halting problem) itself halts. https://leanprover-community.github.io/mathlib_docs/computability/halting.html