Simple proofs using ChatGPT

Stream: new members

[Marcus Smith]

Hi! I'm interested in contributing to mathlib. I recently submitted a PR about the sum of the first n odd numbers, and I’d love to help with other simple math theorems using ChatGPT to write the code so I can help complete formalization of simple proofs.

[Mario Carneiro]

To avoid making unnecessary work for the reviewers, I recommend you read the contribution guidelines and also take a bit of look at other PRs to get a general sense of how PRs are done. You should also learn how to write lean code in general, and try doing a proof on your own of an interesting theorem (and possibly get help here on how to write it). Contributing to mathlib is usually something which comes later, e.g. once you are most of the way through one of the lean introductory textbooks like #tpil or #mil.

While ChatGPT is not exactly banned or even discouraged for some things, it can be very easy to be completely mislead by its outputs as a newcomer. If you try to get ChatGPT to write your PR for you and you don't understand what it is doing, it's almost certainly going to be a bad PR and will probably be closed immediately. Don't do that.