I’m going to participate in the “Autoformalization for the Working Mathematician” workshop. This is a hands-on, multi-day workshop with great talks and a hackathon. I’m sure that many interesting things in the space of Lean and LLM-based agentic AI will emerge from it. I believe that now is the time of automatic Lean, but we’re not quite there yet.