Zulip Chat Archive

Stream: general

Topic: ml methods in interactive theorem proving

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: Dec 20 2023 at 11:08 UTC