AI for Math Summer Fellowship
Overview: The AI for Math Summer Fellowship is a 10-week (June 15 - August 21, 2026) research program placing students within active projects supported by the AI for Math Fund. Seven fellows will be selected to work directly with leading research teams advancing artificial intelligence for mathematics, including work on automated theorem proving, proof assistants, formal verification, mathematical datasets, and open-source research infrastructure. Fellows will be embedded within a host research team while participating in a small cohort of fellows and programming organized by Renaissance Philanthropy’s AI for Math team.
Program activities include:
Program kickoff and orientation session
Ongoing cohort check-ins
Mid-program progress review
End-of-summer presentations
(Pending Date) Participation in the one-day in-person AI for Math convening (London), bringing together fellows, grantees, and researchers across the AI-for-math ecosystem
Across the program, fellows will:
Gain hands-on experience working on AI for math research projects
Contribute technical outputs to active open-source research initiatives
Work closely with leading researchers and developers in the field
Build relationships with peers and mentors across the AI-for-math ecosystem
Compensation: Fellows will receive a $20,000–$30,000 stipend, depending on geography, experience, and project scope. Renaissance Philanthropy will cover travel costs if necessary for fellows who need to temporarily relocate for the placement.
How to Apply: Submit the following materials through this application link:
CV / Resume
Statements of interest and relevant expertise (1–2 paragraphs)
Optional: links to GitHub, research papers, or prior technical work
About Renaissance Philanthropy. Renaissance Philanthropy is a nonprofit organization that fuels a 21st-century renaissance by increasing the ambition of philanthropists, scientists and innovators. We design time-bound, thesis-driven funds led by field experts and inspire talent to take action through playbooks and communities.
About the AI for Math Fund. The AI for Math Fund is a grant program launched by Renaissance Philanthropy to accelerate progress at the intersection of artificial intelligence and mathematics. The fund supports research, open-source infrastructure, datasets, and field-building efforts that advance AI-assisted mathematical discovery, automated theorem proving, and formal verification.
Fellowship Selection
In 2026, the AI for Math Summer Fellowship is offering seven distinct research placements across leading research groups working at the intersection of artificial intelligence and mathematics. Each fellowship corresponds to a specific project with its own scope of work, research objectives, and mentorship structure.
Detailed scopes of work for each fellowship are linked below. Applicants should review these carefully before applying.
In the application form, applicants will be asked to select a first-choice and second-choice fellowship position. Please ensure that you carefully review the scope of work to confirm you meet the requirements and are eligible to work in the listed location (where applicable) before selecting your preferences. Please note that Renaissance Philanthropy is not able to sponsor visas for this fellowship.
| Project Title and Link | PI / Mentor | Description | Eligibility | Location |
|---|---|---|---|---|
| A Dataset of Modern Formalized Theorem Statements | Kevin Buzzard | Use autoformalization tools to formalize modern mathematical results and contribute to a dataset of formalized theorem statements. | Master’s, PhD | Hybrid (London) |
| Bridging AI, Proof Assistants, and Mathematical Data (BRIDGE) | Andrej Bauer | Build tools and interfaces for querying large datasets of formalized mathematics and explore AI methods for structuring mathematical knowledge. | Master’s, PhD | Hybrid (Ljubljana) |
| Constraining LLMs for Theorem Proving: A Neurosymbolic Approach to Guaranteed Autoformalization | Eleonora Giunchiglia / Mihaela Cătălina Stoian | Implement grammar-constrained decoding methods to improve the correctness of LLM-generated formal mathematical statements and proofs. | PhD only | In person (London) |
| Copilots for Isabelle: Learning Logical Structure for a Better Proving Experience | Andrei Popescu / Dmitriy Traytel / Mohammad Abdulaziz | Develop AI copilots for the Isabelle proof assistant, such as tools for generating proofs, documenting code, or tuning LLMs for formal reasoning tasks. | Undergraduate, Master’s, PhD | Hybrid (Sheffield, London, or Copenhagen) |
| Game Over or QED? – Taking the Lean Game Server to the Next Level | Marcus Zibrowius | Formalize undergraduate math exercises in Lean and convert them into interactive game levels with hints and structured learning steps. | Undergraduate, Master’s | Hybrid (Belgrade) or Remote |
| Large Language Models for Lattice-Theoretic Reasoning of Reactive Programs | Pedro Ribeiro | Mechanize lattice-theoretic frameworks for reasoning about reactive programs in Isabelle/HOL and potentially prove new theorems or develop executable semantics. | Undergraduate, Master’s, PhD | In-person (York) |
| MathBench: Towards Evaluating Natural Language Proofs | Pawan Sasanka Ammanamanchi | Build datasets and models to evaluate how accurately AI systems translate informal mathematical statements into formal representations. | Master’s, PhD | Fully Remote |
Diversity
We encourage anyone who is interested in this role to apply, regardless of whether you feel you meet 100% of the qualifications. The top candidates will bring their own unique perspectives, experiences, and backgrounds from a variety of industries along with many but not necessarily all the skills listed above.
Recruiting, hiring, mentoring, and retaining a diverse workforce is critical to our success. All qualified applicants will receive consideration for employment without regard to race, colour, religion, sex, sexual orientation, gender identity, national origin, disability, or status as a protected veteran.
Renaissance Philanthropy is an equal-opportunity employer. We celebrate diversity and are committed to creating an inclusive environment for all employees.