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.

[Siddhartha Gadgil]

A simple Github copilot experience: I had to duplicate Python code in Lean. Pasted it in comments and the Lean code was almost perfectly generated in steps.

[Jason Rute]

@Siddhartha Gadgil I’m a bit confused what you task was that you had copilot do. What do you mean by “duplicate Python code in Lean”. Do you mean translate Python code to Lean code?

[Siddhartha Gadgil]

Yes, write analogous functions

[Siddhartha Gadgil]

I mean the 60 lines starting at https://github.com/siddhartha-gadgil/LeanAide/blob/6702257f1d73ea72206afc76dac0b3e061b248e3/scripts/queries.py#L210 excluding a function
were made into lines starting at
https://github.com/siddhartha-gadgil/LeanAide/blob/6702257f1d73ea72206afc76dac0b3e061b248e3/LeanCodePrompts/ChatClient.lean#L321

[Alex Kontorovich]

Yep! My experience as well, on many occasions... (Hence interweaving the PNT+ blueprint with TeX / Lean mixed together...)