FRESCO is a research project aimed at building a new programming environment for fast and verified symbolic computation.

This project will be generously funded for five years by an ERC Consolidator grant. The core team is located in University of Nantes, in the Gallinette Inria team-project, with some members hosted in Paris Saclay University, in the Toccata Inria team-project.

Contents: News ⋅ Goals ⋅ Members

- 2022-01-01: Delighted to welcome Matthieu Piquerez.
- 2021-11-01: Official start of the project.

Computers have changed the face of research in mathematics. They
have dramatically augmented experiment and guesswork. Groundbreaking
conjectures were only made accessible by resorting to superhuman
computational power, e.g., Mandelbrot's fertile observations in
fractal geometry, or Birch and Swinnerton-Dyer's conjecture, for which
the Clay Institute advertises a $1 million bounty. In fact, they
have also revolutionized the essence of what a proof is. Starting with
the Four Color theorem, about the coloration of planar maps, the list
of **computer-assisted proofs** of major mathematical results has
grown steadily, covering a broad range of mathematical fields:
combinatorics, optimization, number theory, dynamical systems,
etc.

Computer proofs are essentially produced by **symbolic
computations**, on exact data such as (unbounded) integers, rational
numbers, polynomials, matrices. **Computer algebra systems** are
the main vehicle of symbolic methods. Besides the libraries
implementing **cutting-edge fast algorithms**, these complex
systems are also powered by a domain specific language, used to
formulate queries, and sophisticated graphical interfaces, which allow
to produce documents interleaving text and graphics, with
calculations. But *“are we just getting wrong answers faster?”*
Stadtherr's unkind question to the community of high-performance
computing not only remains valid today, but it extends to the realm of
computer algebra. While machine-assisted design and verification have
become standard for critical systems or when security and privacy
issues are at stake, only makeshift techniques are available for
auditing computer-produced mathematics, far behind the current state
of the art in program verification.

New theoretical and practical tools are needed to produce, and
reason about, computer-aided mathematics, with no compromise on speed
nor on reliability. Our grand challenge is thus to deliver **fast yet
reliable symbolic computations** to the users of computer algebra
systems. For this purpose, we will design a novel generation of
mathematical software, based on the firm grounds of modern programming
language theory. In particular, the main vision behind the FRESCO
project is a **verified compilation scheme** from textbook formulas
to machine code, with feedback to formal
proofs. Using Coq's higher-order,
dependently typed, programming language we can express all these
steps, specify and verify each transformation phase, and reuse the
result in a broader formal proof context.

**Chris Hughes**(PhD candidate, co-supervised by Cyril Cohen and Assia Mahboubi)**Assia Mahboubi**(PI)**Guillaume Melquiond**(Senior member)**Matthieu Piquerez**(Postdoctoral researcher)

**Cyril Cohen**(Inria)**Sander Dahmen**(VU Amsterdam)