Proof Engineer, Autoformalisation Engineer
Help Iliad accelerate mathematical research with LLMs, building and running an autoformalisation engine that turns researchers' proposals into faithful formal programmes in Lean.
About Iliad
Iliad is a nonprofit dedicated to advancing foundational AI alignment research. Our research division is made up of several teams working on the mathematical and conceptual foundations of the field, including Learning Theory, Abstractions & Representations, Agency, and Scalable Oversight & Heuristic Arguments. Alongside our own research, we train new alignment researchers through the Iliad Intensive and the Iliad Fellowship, incubate research organizations and an academic journal, and run a range of conferences that bring together researchers working on the hardest problems in AI safety. We're a small and quickly growing team.
About the Role
Iliad wants to accelerate mathematical research with LLMs, with the ultimate goal of producing new mathematics. As a Proof Engineer / Autoformalisation Engineer, you’ll work with researchers to turn research proposals into formal programmes in Lean. You’ll build and operate an autoformalisation engine of coordinated LLM agents, combining mathematical judgement with engineering to make these programmes faithful, useful, and fast to develop.
What you’ll do
- Work with researchers to understand their proposals, clarify their objectives, and identify the supporting mathematics that needs to be formalised.
- Use and develop the engine to produce the definitions, supporting infrastructure, and capstone theorem statements that specify a research programme. These statements set targets for proof.
- Own the engine’s operation, debugging, and optimisation. Ensure definitions and statements faithfully represent both the proposal and the mathematics of the field, and that target theorems are reasonable and intellectually useful steps towards the research objectives.
- Help researchers use the formal programme for difficult calculations, solving equations, and applying existing techniques to concrete domains. Develop it towards the longer-term aspiration of autonomous agents advancing researchers’ agendas and producing new mathematics.
What We're Looking For
- Strong mathematical understanding and judgement: you can grasp research proposals and assess whether a formal programme serves their objectives.
- Lean and formalisation skills to express mathematical ideas faithfully and build the supporting foundations.
- Engineering ability and practical LLM judgement to build, debug, and improve coordinated agents for mathematical research.
Our benefits include:
- Time Off: 25 days paid vacation annually, plus local holidays.
- Flexible Working Hours: We're a distributed organization with employees in a variety of locations and offer flexible working hours.
- Team Retreats: We have occasional in-person team retreats in California and England.