@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.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet But if you take away the number theory textbook, then chances are very good that they would not be able to prove it, even if you give them their entire life to do it. One is a more or less mechanical activity, the other one is not.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet Good luck to the surgeon ;) [just took some random math book from the shelf].
@ChrSzegedy @freekwiedijk @el_keogh @fchollet I'm not saying it is easy, I'm just saying that at least for humans it is much *easier* than finding a proof of a nontrivial theorem, and it could be so for the AI too.