Proof Engineer, Autoformalisation Engineer

Build and operate an autoformalisation engine using LLM agents to turn mathematical research proposals into formal Lean programmes.
- Work with researchers to understand proposals and identify mathematics requiring formalisation into formal programme specifications.
- Own engine operation, debugging, and optimisation to ensure definitions and theorems faithfully represent research objectives.
- Help researchers use formal programmes for calculations, equation solving, and technique application towards autonomous mathematical discovery.
- Requires strong mathematical judgement, Lean formalisation skills, and ability to build and debug coordinated LLM agents.

Iliad is an umbrella organization that advances applied mathematics research in AI alignment through conferences, research incubation, and fellowship programs.