Testimonials

Stream: Machine Learning for Theorem Proving

[Martin Dvořák]

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]

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.