ChatGPT is a great help for programming in standard programming languages. It does not seem to be as good with lean, a program for formalizing mathematical proofs. Is it possible to make it (1) refer to the current version of lean (2) know about the mathematical library available for lean. One problem is that these requirements form a moving target, since the language is in rapid development.
I'm new to lean, and it's possible that what I'm asking for already exists in some form. If it does, please tell me where I can find out about that.
