@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.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet That's why I don't believe that translation of informal proof is more difficult...I think we have to clearly separate the two problems of informal math to formal versus finding proofs.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet There is some overlap for sure but at an advanced level these are very different problems.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I don't think there is much difference. It all depends on the system's sophistication. The more the system "knows", the better it can argue, the bigger gaps it will be able to bridge.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet If you give me any intelligent (say, a surgeon) and sufficiently motivated person, you could put them through a math education and teach them Lean, and given a bunch of time they could formalise the prime number theorem if you give them a textbook.