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 brie y discuss some of our objectives and methods.