Sheffield to lead $1M project on AI-powered theorem proving, funded by Renaissance Philanthropy and XTX Markets
Titled ‘Copilots for Isabelle: Learning Logical Structure for a Better Proving Experience’, will advance the foundations and technology of interactive theorem proving, developing next-generation methods for proof assistants.