For those using @leanprover AI models to “compete” in #imo2025 (@ProjectNumina , @KaiyuYang4), what Lean formalizations will you use? (A) autoformalized statements, (B) manually formalized statements, (C) Joseph Meyer’s IMOLean formalizations (github.com/jsm28/IMOLean)?

At #JMM2025 last week, a mathematician told me he used ChatGPT (forgot which version) to get a major insight into solving his math problem. But, he is reluctant to share publicly (e.g. in his paper) that this happened since it could make him look less bright. I find this sad. 🧵

I’m really excited to announce that I’m going to be at the Joint Math Meetings #JMM2025 to give a talk on AI for Formal Theorem Proving on Friday. Reach out if you want to talk about AI for Math or for all my math friends, if you just want to catch up!

Hot take: For automatic theorem proving (ATP) to solve unsolved math problems, the most important need is auto-formalization. We already have general-purpose reasoning models (o3 and more to come). We need to verify the correctness of these models with absolute certainty. 🧵

Idea: Let’s change all the benchmarks to severely punish an answer if it is wrong. (Blank answers not rewarded or punished.) AI is most useful and most efficient when we know an answer is correct. (1/n)

This was a really enjoyable discussion between OpenAI and @teorth.bsky.social. It was very thoughtful and open, more than I would have expected, with good discussion about the future of math research given AI.

I'm not at NeurIPS this year (and unfortunately never have been), but I just want to say good luck to the MATH-AI speakers and participants today. I hope it is a productive workshop which moves the field forward. I look forward to hearing the highlights.