@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 @ChrSzegedy @el_keogh @fchollet I don't care for in principle. All I want is a nice workflow.
@JulesJacobs5 @ChrSzegedy @el_keogh @fchollet ... without a "type something, WAIT" oscillation.
@freekwiedijk @JulesJacobs5 @el_keogh @fchollet What I envision is that you write an informal natural language text, then after significant wait (maybe minutes), you get a full formalization w/o intervention, or some natural language questions and partial formalizations if it was not successful.