automatic prover

Stream: general

[RexWang]

Hi everyone, I am new to the community. And I am interested in doing automatic things with Lean.
I don't know if there is a way for Lean to directly call AI to assist with generating code or providing next steps. In vscode, the right sidebar only shows the current target and syntax information, and it doesn't seem to have any relevant options.
Any suggestion? Thank you guys!

[Jason Rute]

#Machine Learning for Theorem Proving

[Junyan Xu]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/api.20suggestion.20vscode.20integration/near/298755853 : the rightmost button toggles AI suggestions, notice the graphics is recently changed.

[Jason Rute]

Simple automation includes the tactics library_search, suggest, tidy and probably a few others.

In Lean 3 there are two suggestion features based on AI research projects with large language models.

• #general > ✔ HTPS in vscode? Gives suggestions in sidebar when turned on. Based on a research project of Meta research.
• #lean-gptf A tactic which gives suggestions. Based on a research project of OpenAI and some of us here.

In Lean 4 there is Aesop (let me find a reference) which is a powerful search algorithm which you can customize if I understand correctly.

[Jason Rute]

Aesop: https://github.com/JLimperg/aesop