Dear Colleagues, We are pleased to advertise an AI for Math Summer Fellowship opportunity on the project "Copilots for Isabelle: Learning Logical Structure for a Better Proving Experience". The general call and application details (including an application link) can be found here: https://docs.google.com/document/d/1tXlT2A2NyLi_N-Fn1Q5zwG6J0b8Cwhzj/edit Please note that the application deadline is April 10, and the internship will run for 10 weeks, from June 15 to August 21, 2026. In this project, the selected fellow will work with researchers at the University of Sheffield, University of Copenhagen, and King’s College London on developing AI-based copilots for the Isabelle proof assistant. The aim is to leverage the rich structure of interactive proofs to build intelligent tools that assist with proof development, documentation, and automation. The fellowship offers the opportunity to work on topics such as: -- generating polished proofs from informal or partial drafts, -- automatically producing documentation for Isabelle/ML code, -- adapting and tuning LLMs for proof tasks. The position is open to undergraduate, master’s and PhD students, and can be carried out in Sheffield, Copenhagen, or London (with support for travel if needed). Please see the attached project description for further details. Best wishes, Andrei, Dmitriy and Mohammad