@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.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet It is. OTOH, a single "easy to see" step in a high level textbook can be more complex than a whole statement the prrof pf which is given in an introductuonary text book. And there are multiple levels of "higher level".