Zulip Chat Archive

Stream: general

Topic: automatic prover


RexWang (Dec 15 2022 at 09:26):

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 (Dec 15 2022 at 09:29):

#Machine Learning for Theorem Proving

Junyan Xu (Dec 15 2022 at 09:34):

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 (Dec 15 2022 at 09:37):

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 (Dec 15 2022 at 09:38):

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


Last updated: Dec 20 2023 at 11:08 UTC