Large-Scale Formal Proof for the Working Mathematician -- Lessons learnt from the ALEXANDRIA Project
History and Overview
2023-05-26 v2
Abstract
ALEXANDRIA is an ERC-funded project that started in 2017, with the aim of bringing formal verification to mathematics. The past six years have seen great strides in the formalisation of mathematics and also in some relevant technologies, above all machine learning. Six years of intensive formalisation activity seem to show that even the most advanced results, drawing on multiple fields of mathematics, can be formalised using the tools available today.
Keywords
Cite
@article{arxiv.2305.14407,
title = {Large-Scale Formal Proof for the Working Mathematician -- Lessons learnt from the ALEXANDRIA Project},
author = {Lawrence C Paulson},
journal= {arXiv preprint arXiv:2305.14407},
year = {2023}
}
Comments
Invited paper for CICM 2023 (Conference on Intelligent Computer Mathematics). This revised version adds two references