search

lean-dojo / LeanDojoChatGPT

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

The example path error problem #1

Closed JasonNing96 closed 1 year ago

JasonNing96 commented 1 year ago

Hi, I'm so glad to look this so amazing Idea in math, and I Couldn't wait to try out the invention.

I have install the plugin local and add to my GPT-plugin store, followed the step of Readme. Everthing is fine ,but when I try to prove the example "Hellow world" The plugin returen an error said

"I'm sorry, but it seems there was an issue connecting to the Lean theorem prover. I'm unable to fetch the theorem from the provided file path at the moment.", Please help me solve this trouble, Thanks very much.

image

yangky11 commented 1 year ago

Hi,

I just updated https://github.com/lean-dojo/LeanDojoChatGPT#questions-and-bugs. Could you please follow it to provide additional information, such as debug logs printed by the backend server? Thanks!

yangky11 commented 1 year ago

@Deep0Thinking Is it working now?

yangky11 commented 1 year ago

@Deep0Thinking Please follow https://github.com/lean-dojo/LeanDojoChatGPT#questions-and-bugs. It would be very difficult for me to help with only a screenshot.

yangky11 commented 1 year ago

Closing due to inactivity