search

lean-dojo / LeanDojoChatGPT

ChatGPT plugin for theorem proving in Lean
https://leandojo.org
MIT License
112 stars 14 forks source link

Way to use post-plugins? #5

Closed rnrand closed 6 months ago

rnrand commented 9 months ago

I clicked on the link for GPT plugins and it says:

"We are no longer accepting new Plugins, builders can now create Actions inside of a GPT."

Is there still a way to use LeanDojoChatGPT?

yangky11 commented 9 months ago

It looks like OpenAI has retired the ChatGPT Plugins API in favor of GPTs. It shouldn't be hard to adapt to the new APIs. We won't have the capacity to do it in the near future, but community contributions are welcome.

rnrand commented 9 months ago

It looks like there's even a GPT for creating actions out of plugins:

https://chat.openai.com/g/g-TYEliDU6A-actionsgpt

I asked it to convert LeanDojoChatGPT to an action, but it needs a URL under "servers" and I don't know whether the current approach will work. I'll pursue this further, but suggestions are welcome.

EliottMeng commented 6 months ago

截至今日，我仍无法在gpt4上使用leandojo，可以提供一个具体教程吗，非常感谢

yangky11 commented 6 months ago

Hi @EliottMeng,

The ChatGPT plugin no longer works because OpenAI has changed its APIs. Due to limited bandwidth, we do not plan to update this repo to keep up with OpenAI. However, it should be fairly straightforward for anyone familiar with OpenAI's API to integrate it with LeanDojo in a way similar to this repo.

Best,