The Coq mailing list

[Josef Urban <josef.urban AT gmail.com>]

A bit of a disclaimer:

I don't know how this article was born. My choice of people and topics would be quite different. I would include the Veroff(McCune)/Kinyon team doing miracles in proving some open algebraic conjectures. And authors of the most successful CASC systems ( http://www.tptp.org/CASC/J10/WWWFiles/DivisionSummary1.html ), hammers for ITPs, ML/ITP systems like TacticToe and Tactician, etc. They produce great work with measurable progress, not hype.

As for language modelling, here is a piece from my 4-page response to a bunch of questions (all that I saw):

====================

Q: You have been partially inspired by Andrej Karpathy, who a few years ago trained a neural network to
generate mathematical-looking nonsense that looked legitimate to non-experts.

A: True .
See the link to his blog post in my paper.
More details : It nicely demonstrated that recurrent neural networks can practically without any
modifications generate texts that capture a lot of statistical dependencies even in scientific
writings. On the other hand, an expert looking at the example of a generated "proof" in my recent
paper will see that the neural network has still very little idea about the meaning of the
statements. And this is exactly the reason why it is interesting to critically evaluate such neural
architectures in formal mathematics: It allows us to judge more clearly than on unstructured texts
the capabilities and limits of the chosen learning architecture. And that in turn allows us to
propose improvements and new architectures. A similar virtuous loop as the one in Malarea
described above, but this time still concerning human rather than AI scientists. And that is also
the reason why producing critical evaluations rather than hype is a necessary attribute of true
science and why uncritical hype damages science.

...

A: Our work in this direction goes back at least five years - see the related work in my

CICM paper. In particular, we have been playing with analogy-based conjecturing since
ca 2015, and with the use of linguistic neural methods that can be used to suggest
statements and proofs since ca 2018.

===================

Josef

On Sun, Sep 6, 2020 at 9:00 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

https://www.quantamagazine.org/how-close-are-computers-to-automating-mathematical-reasoning-20200827/