This application is for contract work writing proofs in the Lean theorem proving assistant. Due to funding conditions, applicants must be resident and eligible to work in the UK. We will be reviewing applications on a rolling basis.
Dovetail is an international, distributed team of about half a dozen researchers all engaged in mathematical AI safety research. We work toward producing mathematical definitions, theorems and proofs that we believe will help society better navigate the ongoing creation of transformative AI. You can read more about our research agenda on our website.
We’ve done a small amount of playing around with Lean ourselves, but we’re not entirely sure what we’ll end up finding most useful. Here are some things that we might ask you to help us with.
We know that some areas of Mathlib are more built out than others, but we don’t have a good understanding yet of which ones. Our research tends to be more flexible about exactly which domains of mathematics we’re using, but currently they include: dynamical systems of all kinds, probability theory, information theory, computability theory, algorithmic information theory, measure theory, ergodic theory, abstract algebra.
If you’re interested, fill out this application form! You’re also welcome to email us with any questions. If you are unsure whether to submit an application, we encourage you to err on the side of applying. After that, the rest of the application steps are:
After that, we should have a good sense of whether we’d like to continue working together.
This job is part of an Advanced Research + Invention Agency-funded project.
