@freekwiedijk @ChrSzegedy @el_keogh @fchollet I think that's a comparatively easy problem. I'd say that if you fix the domain, then we probably already know how to do it, given, say, a hundred million dollars :)
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I disagree. I don't think it is is easy to do with most current paradigms. In order to do that even for current literature, you need much simpler, but modern DL/AI and forgetting most of the "classical" methods.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I mean doing this fully automatically. Of course you can hire 1000s of people formalizing things, but that's very scalable and it will not be self-improving.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet I think @freekwiedijk was talking about manual work, but under the condition that however much time it takes, it must not be much more than the time it takes to write the proof in latex.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet (where all human work is counted, including those you hire)
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I don't think humans can formalize 10X slower than it takes to write a paper. It would be more like 1000X for high level math and very few people have the skill or inclination to do it at all.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet I think the 1000X mostly comes from the math paper being able to build on a huge library of known results. If you count the work to latex all that, then I don't think it's 1000X.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet I think 1000X is about fair (but minimum 100X), because high level math has really huge gaps. It can take hours to formalize a single line in an informal proof. And a lot of parts of the proof assume all kinds of isomorphism and analogies that need to expanded.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet The challenge was Masters-level math (textbooks). I think in that case the gap is much smaller. For instance, if you look at what the Lean people have already formalised, I don't think they could write the equivalent textbooks in less than 1% of the time they spent formalising.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet But if a math paper makes a formally invalid move, such as reasoning by analogy, then the factor could in principle be unbounded.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet Why invalid? The only criterion for a paper to be correct is to convince the reader that a formal proof is *possible*. Analogies, etc are perfectly fine if they help the reader just enough.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet Well, whether a reader is convinced depends on the reader and whether they are right to be convinced too. It's not that different from proof assistants: there you can write scripts that generates proofs too, which is what an analogy kind of is.
@ChrSzegedy @JulesJacobs5 @el_keogh @fchollet Informally, proving that a proof is possible is the same as proving. (Yes, I expect that formally there is a difference.)