Lean-auto - Yicheng Qian

Stream: Lean Together 2024

[Sebastian Ullrich]

Uploaded to Google Slides, there seem to be animations: https://docs.google.com/presentation/d/1SsQQzFG1N2YTI0qjI3wvujbdZm_ux3cM/edit?usp=sharing&ouid=103583794275542947786&rtpof=true&sd=true

[Marcus Rossel]

Why is the proof underlined in yellow here?
screenshot

[Joachim Breitner]

I think it was mentioned earlier: SMT interaction doesn’t have proof reconstruction (yet), so to lean there this is a sorry there.

[Joachim Breitner]

Despite technical issues, great talk and great work!
I am wondering about the name. Given that the corresponding component in Coq and Isabelle world is called “hammer” there, and that auto is yet something else (called aesop in Lean world), is the name “Lean auto” for this project still a good choice?

[Sebastian Ullrich]

@Yicheng Qian Thanks for the talk! Let me know if you want the copy above removed and/or later replaced with the video URL

[Rob Lewis]

Yicheng's recorded talk is now live: https://www.youtube.com/watch?v=aR7Wv_CfkB4

[Jason Rute]

I think I've already mentioned this, but when this is ready to publish, I'd love an evaluation of how lean-auto compares against other forms of automation, like Lean Copilot. For example, in our recent Graph2Tac paper for Coq, discussed in #Machine Learning for Theorem Proving > Announcing Graph2Tac, a prover based on Tactician's new API, we do a careful comparison of our AI theorem prover against CoqHammer. (See Figures 5 and 6 in the results section.) Similarly, a few papers compare against SledgeHammer in Isabelle. It seems that AI-based solvers are quickly catching up and beating hammers, and it would be worth more discussion on how to combine the two approaches better. (Of course, the real test is how these systems do in practice and that is as much about their strength as it is useability factors like ease of installation.)