@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 @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.)
@freekwiedijk @JulesJacobs5 @el_keogh @fchollet The emphasis is on *informally* convincing the reader. (w/o a formal proof).