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