Recommendation on Chatbots for Lean4

Stream: new members

[Britt Anderson]

This topic made me reflect on my use of Chatbots to try and help me learn lean4. None of them seem to work very well. The zulip is great, but there are times when you want a more interactive and immediate approach. With much more lean3 than lean4 in the training data I don't find I get legal code all that often. I am wondering if there are any recommendations for which of the commonly available chatbots seem at the present time to be best at giving small snippets of legal lean4 code. Thanks.

[Pim Otte]

Jason Rute recommended Claude Sonnet in this talk, I've been using that with Github Copilot in VSCode. It's not always correct, but it's been occasionally helpful and I've not seen it emit Lean 3 code.