Stream: new members
Nikolai (Apr 05 2021 at 08:09):
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 (Apr 05 2021 at 08:13):
Did you check out Theorem Proving In Lean? #tpil
Nikolai (Apr 05 2021 at 08:22):
I did not. Thanks
Nikolai (Apr 10 2021 at 18:02):
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 (Apr 10 2021 at 18:51):
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 (Apr 10 2021 at 18:52):
leanchecker is the built-in proof verifier, but there are other implementations of programs that verify lean proofs
Chris B (Apr 10 2021 at 18:53):
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 (Apr 10 2021 at 19:03):
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 (Apr 10 2021 at 19:16):
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 (Apr 12 2021 at 18:25):
Thanks for the all the replies. I guess I have a lot of fun reading to do :D
Last updated: May 06 2021 at 22:13 UTC