Status of leanprover-community/llm

Stream: Machine Learning for Theorem Proving

[Joseph Tooby-Smith]

I'm looking for a light-weight way to interact with e.g. chatgpt within Lean code.
One option I have found is leanprover-community/llms. However this is somewhat out-dated (currently on v4.5.0-rc1).

So my question: Has leanprover-community/llms been superseded by something, and if so what?

If it hasn't, I'm happy to make steps to bumping it to the current version of Lean.

[Joseph Tooby-Smith]

(I've made a pull-request bumping leanprover-community/llms to v4.10.0-rc2.)

[Kim Morrison]

I've merged, thank you. As you can see, no one has done any work on that repo in quite some time. If someone would like to, that would be great.

[Kim Morrison]

The idea was to provide a model-agnostic frontend for basic chat functionality, on top of which people could build e.g. autoformalization helpers. But if someone wants to run with it in a different direction, that is completely fine!

[Joseph Tooby-Smith]

Thanks for merging Kim. My current use of it (here) is as a cheap way to check doc-strings for spelling and grammar. It served this purpose well :).

[Kim Morrison]

Nice! :-)

[Siddhartha Gadgil]

Just mentioning that I have code at https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanCodePrompts/ChatClient.lean for calling a few chat servers via API. I would be happy to upstream it to a common library (some of it is very much customized for my use cases though).