Opendata, web and dolomites

ALEXANDRIA SIGNED

Large-Scale Formal Proof for the Working Mathematician

Total Cost €

0

EC-Contrib. €

0

Partnership

0

Views

0

Project "ALEXANDRIA" data sheet

The following table provides information about the project.

Coordinator
THE CHANCELLOR MASTERS AND SCHOLARSOF THE UNIVERSITY OF CAMBRIDGE 

Organization address
address: TRINITY LANE THE OLD SCHOOLS
city: CAMBRIDGE
postcode: CB2 1TN
website: www.cam.ac.uk

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country United Kingdom [UK]
 Total cost 2˙430˙140 €
 EC max contribution 2˙430˙140 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2016-ADG
 Funding Scheme ERC-ADG
 Starting year 2017
 Duration (year-month-day) from 2017-09-01   to  2022-08-31

 Partnership

Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 
1    THE CHANCELLOR MASTERS AND SCHOLARSOF THE UNIVERSITY OF CAMBRIDGE UK (CAMBRIDGE) coordinator 2˙430˙140.00

Map

 Project objective

Mathematical proofs have always been prone to error. Today, proofs can be hundreds of pages long and combine results from many specialisms, making them almost impossible to check. One solution is to deploy modern verification technology. Interactive theorem provers have demonstrated their potential as vehicles for formalising mathematics through achievements such as the verification of the Kepler Conjecture. Proofs done using such tools reach a high standard of correctness.

However, existing theorem provers are unsuitable for mathematics. Their formal proofs are unreadable. They struggle to do simple tasks, such as evaluating limits. They lack much basic mathematics, and the material they do have is difficult to locate and apply.

ALEXANDRIA will create a proof development environment attractive to working mathematicians, utilising the best technology available across computer science. Its focus will be the management and use of large-scale mathematical knowledge, both theorems and algorithms. The project will employ mathematicians to investigate the formalisation of mathematics in practice. Our already substantial formalised libraries will serve as the starting point. They will be extended and annotated to support sophisticated searches. Techniques will be borrowed from machine learning, information retrieval and natural language processing. Algorithms will be treated similarly: ALEXANDRIA will help users find and invoke the proof methods and algorithms appropriate for the task.

ALEXANDRIA will provide (1) comprehensive formal mathematical libraries; (2) search within libraries, and the mining of libraries for proof patterns; (3) automated support for the construction of large formal proofs; (4) sound and practical computer algebra tools.

ALEXANDRIA will be based on legible structured proofs. Formal proofs should be not mere code, but a machine-checkable form of communication between mathematicians.

 Publications

year authors and title journal last update
List of publications.
2018 Manuel Eberl; Lawrence C. Paulson
The Prime Number Theorem
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Anthony Bordg
Projective Geometry
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2017 Wenda Li
Evaluate Winding Numbers through Cauchy Indices
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Angeliki Koutsoukou-Argyraki; Wenda Li
Irrational Rapidly Convergent Series
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2017 Wenda Li
Count the Number of Complex Roots
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Lawrence C. Paulson
Quaternions
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Wenda Li
The Budan-Fourier Theorem and Counting Real Roots with Multiplicity
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2019 Lawrence C. Paulson
Zermelo Fraenkel Set Theory in Higher-Order Logic
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2019 Lawrence C. Paulson
Fourier Series
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Mohammad Abdulaziz and Lawrence C. Paulson
An Isabelle/HOL formalisation of Green\'s Theorem
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Anthony Bordg
The Localization of a Commutative Ring
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2020 Angeliki Koutsoukou-Argyraki
Aristotle\'s Assertoric Syllogistic
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2019 Angeliki Koutsoukou-Argyraki, Wenda Li
The Transcendence of Certain Infinite Series
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2018 Angeliki Koutsoukou-Argyraki
Octonions
published pages: , ISSN: 2150-914x, DOI:
Archive of Formal Proofs 2020-03-11
2019 Li, Wenda; Paulson, Lawrence
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem
published pages: , ISSN: , DOI: 10.17863/CAM.35599
1 2020-01-16
2019 Wenda Li, Lawrence C. Paulson
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL
published pages: , ISSN: 0168-7433, DOI: 10.1007/s10817-019-09521-3
Journal of Automated Reasoning 2020-01-16
2019 Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL
published pages: 69-91, ISSN: 0168-7433, DOI: 10.1007/s10817-017-9424-6
Journal of Automated Reasoning 62/1 2020-01-16
2018 Anthony Bordg
Univalent Foundations and the UniMath Library
published pages: , ISSN: , DOI:
Reflections on the Foundations of Mathematics - Univalent Foundations, Set Theory and General Thoughts 2020-01-16
2018 Mohammad Abdulaziz, Lawrence C. Paulson
An Isabelle/HOL Formalisation of Green’s Theorem
published pages: , ISSN: 0168-7433, DOI: 10.1007/s10817-018-9495-z
Journal of Automated Reasoning 2020-01-16
2018 Lawrence C. Paulson
Formalising Mathematics In Simple Type Theory
published pages: , ISSN: , DOI:
Reflections on the Foundations of Mathematics - Univalent Foundations, Set Theory and General Thoughts 2020-01-16
2019 Anthony Bordg
On a Model Invariance Problem in Homotopy Type Theory
published pages: , ISSN: 0927-2852, DOI: 10.1007/s10485-019-09558-w
Applied Categorical Structures 2020-01-16

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "ALEXANDRIA" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email (fabio@fabiodisconzi.com) and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "ALEXANDRIA" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.1.)

PROGRESS (2019)

The Enemy of the Good: Towards a Theory of Moral Progress

Read More  

OBSERVE (2020)

Overcoming cellular barriers to therapeutic RNA delivery using extracellular vesicles

Read More  

HOLI (2019)

Deep Learning for Holistic Inference

Read More