Body: <p>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.</p>
  <p>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.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2024-09-27T13:50:55.767Z
Comments.Text: You might prefer to ask in https://genai.stackexchange.com/ as this Stack Exchange is about AI theory (e.g. what goes into making an AI system), whilst your question is about getting results from a specific product. There are some cross-overs between the sites for questions that ask about general behaviours or approaches to the products that are based on large language models, such as ChatGPT.
Comments.UserDisplayName: Neil Slater
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2024-09-29T02:44:11.940Z
Comments.Text: This may interest you: https://arxiv.org/abs/2205.11491
Comments.UserDisplayName: bogovicj
Tags: <computer-programming>
Title: Using ChatGPT for lean programming
UserDisplayName: Marcel Bokstedt
ThreadText: # Using ChatGPT for lean programming
  
  (Asked by: username_0 on 2024-09-27)
  
  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.
  
  **Tags:** computer-programming
  
  > **Comments:**
  > **username_1**: You might prefer to ask in https://genai.stackexchange.com/ as this Stack Exchange is about AI theory (e.g. what goes into making an AI system), whilst your question is about getting results from a specific product. There are some cross-overs between the sites for questions that ask about general behaviours or approaches to the products that are based on large language models, such as ChatGPT.  
  > **username_2**: This may interest you: https://arxiv.org/abs/2205.11491  
  
  ---
  
  ## 0 answers
  
  