ml methods in interactive theorem proving

Stream: general

[Andrew Ashworth]

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]

"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]

i wish they had dealt with have statements properly. in a way, they can be regarded as additional lemmas

[Moses Schönfinkel]

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 :).