Imperial mathematician receives grant to formalise theorems with AI The goal is to create a robust resource for future research
