ALEXANDRIA - Large Scale Formal Proof for the
              Working Mathematician

                                          Angeliki Koutsoukou-Argyraki
                                            University of Cambridge
                                               ak2110@cam.ac.uk




                                                        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 for-
                       malizing mathematical proofs with the proof assistant Isabelle. The
                       focus of the project is the management and use of large-scale mathe-
                       matical knowledge, both as theorems and as algorithms. In this talk
                       we will briefly discuss some of our objectives and methods.




Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: O. Hasan, C. Kaliszyk, A. Naumowicz (eds.): Proceedings of the Workshop Formal Mathematics for Mathematicians (FMM),
Hagenberg, Austria, 13-Aug-2018, published at http://ceur-ws.org