Zulip Chat Archive

Stream: Machine Learning for Theorem Proving

Topic: Testimonials


Martin Dvořák (Sep 15 2023 at 12:08):

There are many things going on in Machine Learning for Theorem Proving.
For people who are not actively involved in the development, it may be difficult to keep track of what is an experimental effort and what is already useful.
So I decided to create this thread for testimonials only!
Have you used any ML tools in formalization recently? How did your experience go?

Do not post here:

  • How to install X on Y.
  • How X works internally.
  • I implemented a new features for X.

Please post here:

  • Program X helped me to do Y.
  • Program X failed to do Y.
  • I used X to do Y, but it would have been faster to do Y manually.

Martin Dvořák (Sep 15 2023 at 12:25):

PS: I don't want to compete against threads dedicated to particular programs or tools.
Please feel free to post redundantly; if your experience has relevance for both ordinary Lean users and for AI/ML researchers/developers, please share your experience in both this thread and the dedicated one.
I want this to be a standalone and authentic overview for people who don't follow the other (usually more technical) discussion threads.


Last updated: Dec 20 2023 at 11:08 UTC