PedroMoralesAlmazan
Timothy GowersI will be taking on at least one new PhD student in automatic theorem proving in October 2023. If you might be interested in applying, it is bureaucratically easier if you do so before January 6th, though not completely essential. For more details about the project, have a look at our website, which is still under development but which contains quite a lot of material. 1/
The ideal candidate will be able to demonstrate a keen interest in thinking about how proofs are discovered, and a sensitivity to the difference between the discovery process and the proofs themselves. They will also be a skilled programmer, and ready to work in a team. They should also make clear that they have understood the difference between our approach to automatic theorem proving and other approaches that are current. 2/
In particular, while we hope to interact with those working from a machine-learning perspective, that is not our approach -- we want to go as far as we can writing programs that are explicitly designed to find proofs.
If you yourself are not interested in applying but know somebody who might be, I would be very grateful if you could draw their attention to the opportunity. 3/3
Xavier Généreux@wtgowers To apply should I both send an email and apply through cambridge, or is the email is enough for now?
Also did the sequel of the manifesto mentioned at the end of section 8.1 that is supposed to discuss fully justified proofs available? I would love to read it!
Thank you,
Xavier
James Smith@wtgowers You might be interested in this article by Thomas Hales:
I think that CNL will turn out to be a panacea for formal mathematics.