@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 @freekwiedijk @el_keogh @fchollet Hm, I'm not sure I'd be happy with that...I'd like to give it a formal statement and get a proof of counterproof.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet That's easier, for sure. The system will have that capability, too. Not sure many people will use it though.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet Well I will use it for sure and input the Riemann hypothesis.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet That's why I say that there is a continuum between formalization and reasoning. Early versions of such a system will be able to "formalize" very detailed proofs only, but with time, the system will improve automatically, w/o any extra engineering and get better over time.