@JulesJacobs5 @ChrSzegedy @el_keogh @fchollet The domain is: all math and computer science on the first year master level 😁
@freekwiedijk @ChrSzegedy @el_keogh @fchollet Yes I think we can do that :) Current technology isn't TOO far off from that already, maybe a factor of 10 or so.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I disagree. There is no such technology without conceptual changes. 10X is not a well-defined notion in this context. One can do it but it is not just taking off-the-shelf stuff and changing some measurable aspect of them.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet Why not? I think you can get a factor of 4 already by fixing obvious issues with Coq.
@JulesJacobs5 @ChrSzegedy @el_keogh @fchollet I'm not sure. When I type a lemma statement that "obviously holds" (to me, so it's not really hard to see this), then if I'm correct I want the system to agree *without any further interaction*. I don't think we have that yet, not even slowed down by a factor of 10.
@freekwiedijk @ChrSzegedy @el_keogh @fchollet Hm yes you would need a better Sledgehammer, and various other things, but in order to meet your challenge, I don't think it is necessary for the Sledgehammer to be able to prove all lemmas that you find obvious.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I think that improving classical methods like sledge-hammer is not the right way. They will be solved by purely neural methods that can operate current machinery at a very high level. And I think we are close to that. But it won't be an incremental change to past methods.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet What is the interface to the tool you have in mind?
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet You give it a whole proof text and it will mull it over maybe for minutes and then it comes back either with a formalization candidate for you to revise (if they really care), or with some natural language questions and partial formalizations for the successful parts.
@ChrSzegedy @JulesJacobs5 @el_keogh @fchollet The only proof text I am thinking of is "it is straightforward to show that..." But for the approach that you are thinking of that won't be very useful, I guess 😊
@freekwiedijk @JulesJacobs5 @el_keogh @fchollet That's subsumed too. It might or might not succeed, though, but the capability of the system will improve rapidly over time. In the early stages, I assume it will require more detailed proofs, while after a time of training and feedback, it will cope with mere "easy to see".