Adil Salim

Totally agree with @ErnestRyu that AI helpers will become very useful for research. But in the near future the biggest help will be with *informal* math, the kind we work out with our collaborators/grad students on a whiteboard. I already use frontier models to help write/debug lemmas for my papers and lectures. AI is fast, but can also misunderstand. So have to still carefully check the lemma statements and proofs. But already a big productivity boost. (Lean provers will automate the proof checking, but the human will still need to check that the lean formalization accurately captures their intent, which humans will be doing for a while.)

I'm thrilled to welcome @ErnestRyu to our team in @OpenAI !! If you're excited about the progress we've made in making ChatGPT a useful tool for scientists, just wait for what we'll cook for you next year with @ErnestRyu and the rest of the team!

Totally agree with @ErnestRyu that AI helpers will become very useful for research. But in the near future the biggest help will be with *informal* math, the kind we work out with our collaborators/grad students on a whiteboard. I already use frontier models to help write/debug lemmas for my papers and lectures. AI is fast, but can also misunderstand. So have to still carefully check the lemma statements and proofs. But already a big productivity boost. (Lean provers will automate the proof checking, but the human will still need to check that the lean formalization accurately captures their intent, which humans will be doing for a while.)

100% agree on the productivity boost. One just needs patience to correct mistakes, which are more subtle than before imo. I had a nice interaction with GPT-5-pro while proving a convex analysis lemma: arxiv.org/abs/2510.26647 The model didn’t write the full proof, but the interaction was interesting enough for me to write a short report about it. The report illustrates both the productivity gain and the need for careful proof-checking. The model’s contributions are in blue, and the full chat is in the Appendix. You will see my prompts and how I think, so, no judgement please :) The problem itself has an history in optimal transport (see intro) and comes from a question I was discussing with some UCLA math professors last summer. Simpler than @ErnestRyu's recent result imo, but still very useful in optimal transport!

100% agree on the productivity boost. One just needs patience to correct mistakes, which are more subtle than before imo. I had a nice interaction with GPT-5-pro while proving a convex analysis lemma: arxiv.org/abs/2510.26647 The model didn’t write the full proof, but the interaction was interesting enough for me to write a short report about it. The report illustrates both the productivity gain and the need for careful proof-checking. The model’s contributions are in blue, and the full chat is in the Appendix. You will see my prompts and how I think, so, no judgement please :) The problem itself has an history in optimal transport (see intro) and comes from a question I was discussing with some UCLA math professors last summer. Simpler than @ErnestRyu's recent result imo, but still very useful in optimal transport!