Mahboubi Lab

Research focus

ERC Consolidator Grant · 2020

Fast and Reliable Symbolic Computation

The use of computers for formulating conjectures, but also for substantiating proof steps, pervades mathematics, even in its most abstract fields. Most computer proofs are produced by symbolic computations, using computer algebra systems. Sadly, these systems suffer from severe, intrinsic flaws, key to their amazing efficiency, but preventing any flavor of post-hoc verification. But can computer algebra become reliable while remaining fast? Bringing a positive answer to this question represents an outstanding scientific challenge per se, which this project aims at solving. Our starting point is that interactive theorem provers are the best tools for representing mathematics in silico. But…

From the public funding record at EU CORDIS. Describes the funded project, not the reviews below.