# Workshop on Algebra, Geometry and Proofs in Symbolic Computation

December 7 - 16, 2015, The Fields Institute

## Overview

The focus of this workshop is on algorithms for polynomials, and their certification, having in mind the geometric study of algebraic and semi-agebraic sets and their applications.

#### Algebraic Algorithms for Polynomials

Solving systems of polynomial equations is a fundamental problem in computer algebra, with applications in many areas. In recent years, algorithms for polynomial system solving have been applied in domainsas diverse as cryptology (through attacks on several multivariate cryptosystems, computations of discrete logarithms in finite elds or on elliptic curves), statistics, the formal verification of programs and many other areas. Popular approaches include of course Grobner bases computations, but also triangular decomposition algorithms, or methods based on toric geometry for sparse systems.Recently there have been a series of improvements in both algorithms and implementation, resulting in orders of magnitude faster performance, systems which were out of far reach a few years ago being now routinely solved.

#### Computations in Real Algebraic Geometry

Real algebraic geometry mainly concerns the study of semi-algebraic sets. Computational aspects in real algebraic geometry are renewed by connections with other areas of mathematics and computer science, such as optimization, control theory robotics, computer aided geometric design, incidence theory and game theory. Recently, there has been significant progress in many problems, such as the quadratic and symmetric case, road map computation and constructive aspects in Hilbert's 17th problem. Much attention is given to certificates of positivity using Bernstein bases, or sums of squares, with connections to semi-definite programming.

#### Certified Algorithms, Computer Algebra and Proofs

Formalization of mathematics is currently a very active topic. There is progress on the foundational aspect as well as on the formalization of significant mathematical results. The impact on computer algebra is both theoretical, since constructive mathematics can help clarifying delicate algorithmic issues in computer algebra, and practical with the integration of computer algebra software and proof assistants. The impact of proof assistantson closely related areas such as computer-assisted manipulations and proofs of combinatorial identities, simplification of hypergeometric sums and more general special function expressions as well as computations in algebraic topology will be also discussed.

On-line registration is open until December 1, but also on-site during workshops. $100 registration fees; students and PDF are $50.

## Schedule

09:00 to 09:55 |
Numerical Schubert Calculus
Frank Sottile, Texas A&M University |

09:55 |
Algorithms to Compute Characteristic Classes of Subschemes of Certain Toric Varieties
Martin Helmer, U.C. Berkeley |

11:10 |
Equivariant Gröbner bases
Robert Krone, Queen's University |

14:40 |
Numerically computing Galois groups
Jose Rodriguez, University of Chicago |

15:55 |
Sparse Eliminants vs Sparse Resultants
Carlos d'Andrea, Universitat de Barcelona |

09:00 to 09:55 |
Sparse polynomial systems with many positive solutions from bipartite simplicial complexes
Pierre-Jean Spaenlehauer, Inria |

09:55 |
Separation bounds for polynomial systems
Elias Tsigaridas, INRIA Paris |

11:10 |
Sparse-FGLM and Linear Recursive Multidimensional Sequences
Jean-Charles Faugere, Inria |

14:40 |
Limit Points of Constructible Sets
Marc Moreno Maza |

15:55 |
Abstract local Bezout theorems and other constructive aspects of Henselian rings
Mari Emi Alonso |

09:00 to 09:55 |
Computing intersections of two algebraic plane curves : the price of the certification
Fabrice Rouillier |

09:55 |
Quantifier elimination for real closed fields : a purely algebraic variant of CAD
Marie-Francoise Roy, Université de Rennes 1 |

11:10 |
On the computation of the silhouette of an analytic surface
Guillaume Moroz |

13:40 to 14:40 |
Application of geometric programming in polynomial optimization
Mehdi Ghasemi, University of Saskatchewan |

14:40 |
Geometry and Symbolic Computation for Analyzing the Singularities of Parallel Robots
Michel Coste, Universite Rennes 1 |

15:55 |
On nearly optimal algorithms for computing roadmaps
Mohab Safey El Din |

09:00 |
Degree bounds in sums of squares representations
Greg Blekherman, Georgia Tech |

09:00 to 09:55 |
On the Complexity of Solving Polynomial Systems via Projection
Michael Sagraloff, Max Planck Institute for Informatics |

09:55 |
A zero counting symbolic procedure for a class of univariate Pfaffian functions
Gabriela Jeronimo, Universidad de Buenos Aires |

11:10 |
Sums of squares on projective varieties
Rainer Sinn |

14:40 |
Complexity of constructible sheaves
Saugata Basu, Purdue University |

15:55 to 16:55 |
Numerical methods for computing real and complex tropical curves
Cynthia Vinzant, North Carolina State University |

16:55 |
Topological complexity of symmetric semi-algebraic sets
Cordian Riener, Aalto University |

09:00 to 09:55 |
A certificate for semidefinite relaxations in computing positive-dimensional real radical ideals
Lihong Zhi, Chinese Academy of Sciences |

09:55 |
Continuous Amortization: Intrinsic Geometric Complexity for Subdivision-based Algorithms
Michael Burr, Clemson University |

11:10 |
Local decomposition and local methods for analyzing real solutions
Jonathan Hauenstein, University of Notre Dame |

09:00 to 09:55 |
The formal proof of the Kepler Conjecture
Tom Hales, University of Pittsburgh |

09:55 |
Cylindrical Algebraic Decomposition with logical structure
James Davenport, University of Bath |

11:10 |
Functional Programming and Complexity
Francis Sergeraert, Institut Fourier |

13:45 to 14:40 |
The Babylonian vs. the Greek Approaches to Computer Proofs
Doron Zeilberger, Rutgers University |

14:40 |
Meta-mathics
Bruno Buchberger, Johannes Kepler University Linz |

15:55 |
Hidden gems of formal combinatorial proofs
Georges Gonthier, Microsoft Research |

09:00 to 09:55 |
Geometric theories for constructive algebra
Henri Lombardi |

09:55 |
Symbolic summation for particle physics: difference ring theory, stable software and proof certificates
Carsten Schneider, Johannes Kepler University Linz |

11:10 |
An exercise in formal proofs for bijective combinatorics
Assia Mahboubi, Inria |

13:45 to 14:40 |
Symbolic Determinant Evaluation
Christoph Koutschan, OEAW |

14:40 |
Table Maker's Dilemma for Transcendental Functions
Nicolas Brisebarre, CNRS, LIP, ÉNS Lyon |

15:55 |
Theorema 2.0: A Brief Introduction and a Case Study in Auction Theory
Wolfgang Windsteiger, Johannes Kepler University |

09:00 to 09:55 |
Rendering useful formalized mathematics
Jesús Aransay |

09:55 |
Formalized mathematics: proofs of transcendence, especially pi
Yves Bertot, Inria |

11:10 |
Leveraging the structure of theory libraries
Jacques Carette, McMaster University |

13:45 to 14:40 |
A Coq formalization of a sign determination algorithm in real algebraic geometry
Cyril Cohen, Inria |

14:40 |
A Comparison of Approaches for Incorporating Syntax-Based Mathematical Algorithms into Proof Assistants
William Farmer, McMaster University |