Re:What the Tortoise Said to Achilles (1895)
by hyp0 on Thursday October 02, 2014 @01:31AM
(#8399535)
EDIT one danger with a library is it might have a theorem stronger than what you're trying to prove (and that you aren't convinced yet by). If it's applied automatically, it's not a convincing proof. (And the purpose here is to be convincing, not just to be correct).
The easy answer is for the user to only allow libraries that they've accepted.
I was thinking we might have an automatic check, that we never use a theorem which is stronger than the whole thing we're trying to prove - that is, which implies our whole proof). But that seems hard to check automatically (maybe undecidable in general).
The easy answer is for the user to only allow libraries that they've accepted.
I was thinking we might have an automatic check, that we never use a theorem which is stronger than the whole thing we're trying to prove - that is, which implies our whole proof). But that seems hard to check automatically (maybe undecidable in general).