Andrew Ashworth (Jun 14 2018 at 04:58):
interesting paper here: "GamePad: A Learning Environment for Theorem Proving" https://arxiv.org/abs/1806.00608
unfortunately the conclusion is the same as it has been for the past 30 years... not quite there yet, needs more funding and research :)
Moses Schönfinkel (Jun 14 2018 at 07:24):
"We also note that position evaluation <omitted> should assign a high number to proof states which do not yet contain the requisite hypotheses to prove the current goal." This metric (representing how far someone is from completing a proof) seems so silly - sadly I can't check how well this works in practice without compiling their entire project because their results sub-chapter doesn't say much :(.
Andrew Ashworth (Jun 14 2018 at 11:35):
i wish they had dealt with
have statements properly. in a way, they can be regarded as additional lemmas
Moses Schönfinkel (Jun 15 2018 at 08:01):
I can't get it to compile. I wanted to check how many steps would be predicted for FLT to reaffirm myself in the belief that this is an incredibly random metric :).
Last updated: Aug 03 2023 at 10:10 UTC