search

siddhartha-gadgil / LeanAide

Tools based on AI for helping with Lean 4
Apache License 2.0
65 stars 5 forks source link

Lean-chat++ #12

Closed ayush1801 closed 2 years ago

ayush1801 commented 2 years ago
  1. Caching of the input prompts in python code/tweaking the lean3 code to save the input prompts
  2. Support chat interface like lean-chat
  3. Adding key-word based prompts
  4. Reverse the prompts in order to keep the most similar example prompt closer to the main prompt.
  5. Developing a trusted server for the HTTP requests - MS Azure, Google cloud etc.
siddhartha-gadgil commented 2 years ago

@0art0 @ayush1801 if everything is done (except the server, which will be done anyway) please close this issue.