This is the website for an automatic theorem proving project funded by the Astera Institute. It is based in Cambridge, but we are open to remote collaboration with others who may be interested. The focus will be on traditional programming methods, but we hope and expect that some of the work we do will have the potential to feed into approaches based on machine learning.
For a short description of our aims, see our About page. For much more detail, the Resources page contains several links to further material of various kinds. On the People page you can see who is involved in the project so far -- further names will be added soon, and if significant external collaboration begins to happen, we will add names of remote collaborators as well. If you are interested in participating, then the Ways of participating page has some suggestions. That page is still very much under construction: in due course we hope to have pages that set out as precisely as possible what our short-term aims are, and what the obstacles seem to be that stand in the way of further progress.
We see the blog as a place where people can post their thoughts when they are sufficiently organized to present in that form. There will be blog posts of several different kinds such as basic tutorials, descriptions of theorem-proving algorithms, talking through specific mathematical problems and how solutions might be discovered, and discussions of theoretical questions connected with automatic theorem proving. If you are interested in contributing a post to the blog, feel free to get in touch.