A computer program can also be considered a form of constructive proof. One may be confident that the program functions as intended until a bug is discovered. This is why theorem provers have such a strong type system, which reduces the likelihood of bugs compared to mainstream programming languages. However, it is important to note that bugs may still be present, just as they can be found in formal proofs on paper.
Do they have a strong type system? Maybe I just haven't gotten to that. My issue is that, there doesn't seem to be any rules for "evaluating" a proof to see if it is valid. Everything seems subjective? Maybe I'm just missing something. But coming from programming, I'm obviously used to a situation where I can put my code through a mechanical evaluator which will tell me if it works. Or at least, will tell me if the syntax is right!
When you proove something you are esentially prooving that a statement logically follows from some other statement(s) for which we know that are true
You can evaluate the validity of a proof by checking the truthfulness of every statement which was used to argue that the proof holds
Miniature example of a proof with relaxed rigor:
Proove that 3+0=3
Proof:
The above statement is a direct consequence of the additive identity axiom which states that x+0=x, if x is a real number. So the only thing we need to check is if 3 is a real number, and we know that it is. The statement holds, end of proof
So to check the validity of this proof you could check if that axiom really exists and check if 3 is a real number, if some of those is false than the proof is invalid
Edit: Or imagine that you have a DB full of axioms, theorems, prooven statements which you can use to proove a given statement. Then you could proove something by just referencing those. Eg. in the example above lets say that the neutral identity axiom has id 3, and the fact that 3 is a real number has an id 103. Then I could just say since 3 and 103 3+0=3
