Abstract: ALEXANDRIA is a new ERC project at the University of Cambridge led by Lawrence Paulson aiming at the creation of a proof development environment for working mathematicians through a collaboration of mathematicians and computer scientists. This will be achieved by formalizing mathematical proofs with the proof assistant Isabelle.
The focus of the project is the management and use of large-scale mathematical knowledge, both as theorems and as algorithms. In this talk we will briefly discuss some of our objectives and methods.
See: http://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/
We will have tea and biscuits in the common room from 10am, the talk will start at 10:30. Please bring a mug if you can. We will also go for lunch after the talk.