clarify (beginner) thinking about automated proof checking

Stream: new members

[rzeta0]

I'm still new to the theory behind how an automated proof checker works - and I've been mulling some of the concepts in my head.

I wanted to check a specific point.

By using propositions as types, we change the problem of proof verification from something more complex to one of checking for "existence".

That is, we find a value of the Proposition type. And if that proposition (proof statement) type is inhabited, we have one (of possibly many) proofs.

The proof checker then checks the type of the proof, which is simpler than other kinds of proof checking (which I don't know about but assume are more complex like grammar checkers for DSLs, compilers for high level languages).

Is this a correct way to think about it?

[Niels Voss]

Checking proofs written in English or another natural language would be a tremendously difficult task for a computer, so in that sense Lean is reducing the extremely complex task of checking English proofs to simply type checking computer programs.

But I'm not sure Lean's type checking is significantly easier than other types of formal proof checking. Formal deduction systems like natural deduction and the sequent calculus are relatively easy to check, and so are other proof systems used by non-propositons-as-types proof assistants like Metamath and Isabelle. I haven't studied any of those in detail, but I suspect they are comparable in difficulty to Lean's proof checking.

[Edward van de Meent]

i guess the motivation to use leans type system rather than those others is the expressivity that it has

[rzeta0]

thanks for the replies.

the comments about type-checking the proof has made me realise I was in error in thinking the problem is one of "existence", of finding an inhabitant of the proof objective's proposition type.

thanks again for helping me correct my thinking

(currently learning Haskell before I go back to the big theory book on type theory)

[Niels Voss]

No, you were absolutely correct that Lean encodes the statement "P is true" as the problem of finding an inhabitant of the type P. I was just disagreeing with the statement that Lean is necessarily significantly simpler than other forms of formal proof checking.