What's a good resource talking about how checking the correctness of proofs works in Isabelle?

It depends what you really want (how does the core work abstractly? how exactly? what should reviewer check in a development? HOL-Proofs?). Maybe @Lawrence Paulson's blog post on LCF?

@Mathias Fleury

That blog post looks good. Basically I need it on a level where someone not familiar with proof assistants gets an idea why to believe machine-checked proofs

Depends on how much detail you want. Possibly useful are this little example and this historical paper. One can also distinguish technical perspectives (formalisms and their properties) from informal ones (the ability to simply read a proof script).

I always say in my talks that internally, every proof gets broken down to the most basic logical inferences (such as modus ponens) and fed through a small kernel that only understands these basic inferences and is thus relatively trustworthy.

I think that's close enough to the truth to be valid for a talk to non-specialists.

Lawrence Paulson said:

Depends on how much detail you want. Possibly useful are this little example and this historical paper.

I will take a look.

Manuel Eberl said:

I think that's close enough to the truth to be valid for a talk to non-specialists.

The context of me asking is that I am currently writing my bsc thesis where I formalized something in Isabelle and in the introduction/prelims after giving a bit of context on Isabelle and how the proving workflow works, I wanted to give a few words about why we can believe that if we proved something in Isabelle, then it's true.

Then perhaps also check with your advisor how much on that topic they want to have in the thesis. I would imagine some (e.g. theorem proving people) will think you shouldn't talk about this at all whereas others (e.g. non-theorem-proving people) will think it's very important.

@Manuel Eberl Yeah, we talked about it. It falls into the latter case

Last updated: Dec 07 2023 at 20:16 UTC