Good conferences and workshops to attend

Stream: Machine Learning for Theorem Proving

[Chiung-Yi Tseng]

Hey I'm a newbie. What's your favorite conferences/workshops in AI4Math field? I'm thinking about Lean users workshop and Neurips. What else?
(I know, this place is for formal proof. But if you know some good "non-formal" events, welcome to DM me.)

[Kaiyu Yang]

You might be interested in this: https://mathai2025.github.io/

[Jason Rute]

For Lean related conferences, there is a list here: https://leanprover-community.github.io/events.html. Some are online and free. Others require travel and/or an invitation. Some have videos and papers. Others don't.

[Jason Rute]

For AI-for-math and AI-for-theorem-proving conferences/workshops.

• The standard AI conferences like neurips, icml, and iclr often have associated workshops on AI for Math. The next is https://mathai2025.github.io/ (as Kaiyu said). They used to be fringe, but now they are very well attended. (They are expensive, but if you don't attend, you can still read the papers after they are released.) Similarly, there are sometimes tutorials on this or related topics at the conference (not part of the workshop).
• AITP (https://aitp-conference.org/) is a classic conference series on AI for theorem proving, which is very casual. It includes a lot of proposals, ideas, and solutions that are not big enough for a full conference paper.
• Harvard CMSA's New Technology in Math seminar invites weekly speakers to discuss lots of things in AI and math. It meets during the semester both at Harvard and on Zoom. (Their webpage is hard to navigate, but the best way to get informed is to reach out to the organizer, Michael Douglas.). They also record their talks on YouTube.
• The Joint Math Meetings, at least this past one, but probably in the foreseeable future, has sessions on both AI for Math and sessions on Lean.
• There are constantly little workshops here and there about AI for math or AI for interactive theorem proving (or even AI for Lean specifically). Some are on the Lean conference list above. Others are announced in #announce. Some are run by mathematicians. Others by computer scientists or programming language researchers. Others by AI researchers. Some have a good showing of people from AI labs. Other none.

[Kaiyu Yang]

Jason Rute said:

They are expensive, but if you don't attend, you can still read the papers after they are released.)

In addition to the usual travel costs, NeurIPS requires workshop attendees to register for NeurIPS, and the pricing depends a lot on whether you're a student or academic. This year, we're exploring whether it's possible to secure a limited number of travel grants.

Yeah, the video recordings will be released some time after the conference.