@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?
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet In theory, the reader always has all the information to prove anything, even w/o the paper. What I mean here is that informal proofs can exploit uncertainty in a non-trivial way, without constructing the proof in any obviously reproducible manner.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet The script could use random numbers too. I think the reader must be able to really construct a proof, otherwise they may have had the emotion of being convinced but this was a mirage.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet The (enough) readers having the feeling of understanding is the only current criterion for a paper to be considered being correct.
@ChrSzegedy @freekwiedijk @el_keogh @fchollet Well, that's just a practical limitation of meatspace humans. With proof assistants we can do better.
@JulesJacobs5 @freekwiedijk @el_keogh @fchollet Sure. That's my goal too. I just wanted to highlight that current notions of correctness do not trivially match that of formalizability. There is a lot of ambiguity etc. that we need to accept of we want to create a fully automated system that can formalize natural language math.