Skip to main content

Questions tagged [errors]

Questions regarding software errors during the usage or development of Proof Assistants.

Filter by
Sorted by
Tagged with
3 votes
2 answers
380 views

How do you know a formal proof (mechanized within a Proof Assistant) really is correct?

Running a proof assistant as a user and focusing on a given formal proof, how can one assert that there are no unexpected errors or "bugs" that could invalidate the provided proof? More ...
taylor.2317's user avatar
  • 1,318