4 Year GTA - Systematic and AI-Assisted Solving of Polynomial Diophantine Equations

About the Project

Open to UK Applicants only

Mathematics are offering 3 fully-funded Graduate Teaching Assistant (GTA) PhD studentships available for UK applicants, starting in September 2026.

Graduate Teaching Assistantships allow research students to fund their PhD through part-time teaching work with the University.

A Graduate Teaching Assistant is responsible to the Head of School and is expected to undertake teaching or other duties within the School - not normally exceeding 8-10 contact hours per week - while undertaking research leading to a PhD.

Approximately 80% of their time will be spent on their doctoral research and 20% on their GTA responsibilities. Training is provided to help Graduate Teaching Assistants develop their teaching related skills and enhance their professional competencies.

Project highights

• Tackle the smallest open Diophantine equations in the systematic programme and convert solved cases into publishable results.
• Formalise selected proofs in Lean and build reusable verified proof patterns for Diophantine arguments.
• Improve the automatic solver and test AI-assisted workflows for discovery, verification and software development.

Project description

This project will continue the programme of solving polynomial Diophantine equations systematically, initiated in book [1] and the accompanying arXiv open-problem list [2]. The guiding idea is to order equations by an appropriate notion of size and attack the smallest unresolved cases first. This creates a transparent pipeline from elementary examples to genuinely difficult problems, and generates publishable challenges that are easy to state but require new number-theoretic, computational and formal methods to solve.

The student will work on selected open problems from the current list [2], aiming either to solve them completely, reduce them to known classes, or produce rigorous evidence and conjectures. The work will combine classical tools (local obstructions, descent, factorisation, modular methods, elliptic curves and computational number theory) with new tools developed specifically for this project. A second strand will formalise selected solved cases in Lean [3], building reusable libraries and proof patterns for Diophantine arguments. A third strand will extend the existing automatic Diophantine-equation solvers [4] by adding methods, benchmarks and a documented database of solved/open instances.

The project will also evaluate how AI tools can accelerate mathematical discovery, proof engineering and software development, while maintaining rigorous verification. Expected outputs include research papers, Lean formalisation artefacts, improved solver functionality and benchmark data, supporting CMS strengths in mathematical AI, automated reasoning and reproducible computation.

Project enquiries to Dr Bogdan Grechuk bg83@leicester.ac.uk

Application enquiries to pgrapply@le.ac.uk

To apply please refer to the application advice and use the application link athttps://le.ac.uk/study/research-degrees/funded-opportunities/maths-gta

Start 21 September 2026

Funding Notes

The 4 year GTA funded studentships provide:

• A combined teaching and stipend payment, currently. for 2026/7 this will be £21,805 per year, paid in monthly instalments
• Tuition fees at UK rates

References

[1] B. Grechuk, Polynomial Diophantine Equations. A Systematic Approach, Springer, Cham, 2024, https://doi.org/10.1007/978-3-031-62949-5
[2] B Grechuk, A systematic approach to Diophantine equations: open problems
arXiv preprint https://arxiv.org/abs/2404.08518
[3] The Lean FRO, The Lean Language Reference, official Lean 4 reference manual, https://lean-lang.org/doc/reference/latest/
[4] Diophantine equations solver http://18.170.245.68/