@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.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet The difference between refereeing to an analogy and writing a script is that a human proof is considered to be correct if it convinces the reader, a mere hint is enough. While a script contains *all* the information to generate the proof.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet Presumably the convinced reader also has the information to generate a proof, right?