NLProof Engineer, Autoformalisation Engineer
IliadRemote
Global catastrophic risksAI safetySoftware engineeringResearch
Why this is on the board
Mathematical research on the safety of AI systems depends on proofs that actually hold, and checking them by hand can cost researchers months. If you build a system that turns their proposals into proofs a computer can check (in the proof language Lean), every researcher who uses it works faster and with less chance of a hidden error.
This board is in beta and this is our judgement. If you think we have it wrong, tell us. Give feedback · How we reason about it
About the role
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 applicatio…
Want to understand this first?
Start with our free course: about 100 minutes in six short units, at your own pace, with no sign-up. To go further, apply for the EA Fellowship: five weeks of reading and discussion in a small group. Also free, but selective.