introductory texts on formalised proofs

Stream: new members

[Nikolai]

Hi Lean community,

I came here via the natural numbers game - which is awesome! many thanks to the creators.
The idea of lettings computers check proofs is very appealing, but only if one understands how the computer does it.
Can you recommend some literature to get me started on that understanding? Or a list of topics that one would need to know to understand how lean works?
My background is a BSc in math.

[Kevin Buzzard]

Did you check out Theorem Proving In Lean? #tpil

[Nikolai]

I did not. Thanks

[Nikolai]

Thanks for the suggestion again. I skimmed it and it looks interesting but is not what I was looking for.
What I'm interested in is more: how proof verification is actually implemented (≈ how is Lean or something similar implemented)?
And the philosophical side: it seems like we would be replacing trust in humans ability to verify specific mathematical proofs for humans ability to verify the proof-checker (lean). Why is that better? How reliably can the verification be verified and what's the formal system for doing so?

[Eric Wieser]

Lean is a lot more than just a proof checker; there is no need to verify tactics or the elaborator, only the kernel itself

[Eric Wieser]

leanchecker is the built-in proof verifier, but there are other implementations of programs that verify lean proofs

[Chris B]

To your second question, I think it's sort of the same reason why it's more appealing to verify that a function sum computes the sum of its arguments and then trusting the results it produces rather than trying to verify the result every time you call it with new arguments. In terms of the actual verification, if you start with some simple-ish set of rules and only allow the entity doing the proving to move according to the pre-approved rules, then chasing some statements back to the axioms of whatever system you're working in requires a number of steps that humans can't handle even if you assume they won't make stupid mistakes (which they will).

[Chris B]

I think metamath has the record for 'simplest implementation of an ITP verifier', the Python one is 370 lines.

hol light is another small/mature prover with a paper that seems to address soundness and construction

metamath-zero is way down in the nitty gritty of implementation and trust for theorem proving, so it may be of interest. There's a companion paper explaining the theory as well.

[Bryan Gin-ge Chen]

In terms of type theory background, I found Nederpelt and Geuvers's "Type Theory and Formal Proof" fairly enlightening, though as an introductory text, it doesn't cover CIC (calculus of inductive constructions, some variant of which is used in Lean's foundations, I believe).

[Nikolai]

Thanks for the all the replies. I guess I have a lot of fun reading to do :D