So this is all great, but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan? These seem like uniquely fragile software artifacts, despite the excellent and robust promises made by the runtime.
> but given that we’re being asked to accept 500k+ line Lean proofs that check but could easily have major semantic errors hidden in them, what’s the plan?
What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.
There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.
There are things you can do in lean which are footguns. For example, 1/0 = 0 in lean. For much of math that's not a problem. Still though, you have to remember that this is the case for whatever number system you're doing a proof in. For things which map to real world scenarios it's potentially a big problem.
1/0 is 0 in lean, though it may not be a problem.
<a href="https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/" rel="nofollow">https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
So, you think it's important for other people to learn Lean's model of type theory before using it to do entirely unrelated proofs, but you see no reason you should know anything about how basic arithmetic works?
thom · · focus · HN ↗
thaumasiotes · · focus · HN ↗
What does it mean for a semantic error to be "hidden in" a proof? The proof has premises and a conclusion, and if you trust the lean kernel it isn't possible for the innards of a proof to contain an error of any kind.
There could be a semantic mismatch between the statement you claim to have proved and the statement that the proof proves, but that has nothing to do with what's inside the proof - it's all right there on the surface.
dnautics · · focus · HN ↗
fooker · · focus · HN ↗
howling · · focus · HN ↗
1/0 is 0 in lean, though it may not be a problem. <a href="https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/" rel="nofollow">https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
thaumasiotes · · focus · HN ↗