# Program

#### Monday 26

9:30 - 10:00 | Welcome | |

10:00 - 11:00 | Claire Tête | Invited tutorial: Depth, dimension and resolution in Commutative Algebra |

30min break | ||

11:30 - 12:30 | Alain Herremann | Invited talk: How to define constructivity? Some few things we can learn from history. |

lunch break (1h45) | ||

14:15 - 15:15 | Claude Quitté | Invited talk: Playing with monomials of k[X_1, …, X_n] |

15:15 - 16:15 | Konstantin Mischaikow | Invited tutorial: Towards an Algebraic Framework for Nonlinear Dynamics |

45min break | ||

17:00 - 18:00 | Timothy Gowers | External event: Fully automatic problem solving with human-style output. |

#### Tuesday 27

9:00 - 10:00 | Claire Tête | Invited tutorial: Depth, dimension and resolution in Commutative Algebra |

10:00 - 10:30 | Francis Sergeraert | Contributed talk: Spectral Sequences downgraded to elementary Gauss Reductions |

30min break | ||

11:00 - 12:00 | Frédéric Chyzak | Invited talk: A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3) |

12:00 - 12:30 | Anders Mörtberg and Cyril Cohen | Contributed talk: Formalizing elementary divisor rings in Coq |

lunch break (1h45) | ||

14:15 - 15:15 | Noam Zeilberger | Invited talk: Refining the meaning of types |

15:15 - 15:45 | Xavier Caruso, David Roe and Tristan Vaccon | Contributed talk: Tracking p-adic precision |

15:45 - 16:15 | MAP meeting | |

Evening | MAP dinner |

#### Wednesday 28

9:00 - 10:00 | Konstantin Mischaikow | Invited tutorial: Towards an Algebraic Framework for Nonlinear Dynamics |

10:00 - 10:30 | Marc Giusti and Jean-Claude Yakoubsohn | Contributed talk: Multiplicity hunting and approximating multiple roots of polynomial systems |

30min break | ||

11:00 - 12:00 | Luca Moci | Invited talk: Matroids over a ring: motivations, examples, applications. |

12:00 - 12:30 | Alain Giorgetti, Richard Genestier and Valerio Senni | Contributed talk: Software Engineering and Enumerative Combinatorics |

lunch break (1h45) | ||

14:15 - 15:15 | Christophe Raffalli | Invited talk: Hilbert's 17th problem via cut-elimination |

15:15 - 16:15 | Claire Tête | Invited tutorial: Depth, dimension and resolution in Commutative Algebra |

#### Thursday 29 is a French holiday.

#### Friday 30

9:00 - 10:00 | Konstantin Mischaikow | Invited tutorial: Towards an Algebraic Framework for Nonlinear Dynamics |

10:00 - 10:30 | Peter Schuster | Contributed talk: Eliminating Krull's Lemma for Horn Clauses |

30min break | ||

11:00 - 12:00 | Ana Romero | Invited talk: Spectral sequences for computing persistent homology |

12:00 - 12:30 | Philippe Malbos | Contributed talk: Linear rewriting and homology of associative algebras |

lunch break (1h45) | ||

14:15 - 15:15 | Grant Passmore | Invited talk: Exact global optimization on demand |

15:15 - 15:45 | Bas Spitters | Contributed talk: Constructive algebra and geometric mathematics |

15:45 - 16:15 | Bruno Grenet | Contributed talk: Computing low-degree factors of lacunary polynomials: a Newton-Puiseux approach |

### Abstracts

#### Frédéric Chyzak: *A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)*

We report on the formal verification of an irrationality proof of the evaluation at 3 of the Riemann zeta function. This verification uses the Coq proof assistant in conjunction with algorithmic calculations in Maple. This irrationality result was first proved by Apéry in 1978, and our formalization follows the proof path of his original presentation. The crux of it is to establish that some sequences satisfy a common recurrence. We formally prove this by an a posteriori verification of calculations performed by a Maple session. This bases on computer-algebra algorithms implementing Zeilberger's approach of creative telescoping. This experience illustrates the limits of the belief that creative telescoping can discover recurrences for holonomic sequences that are easily checked a posteriori. We discuss this observation and describe the protocol we devised in order to produce complete formal proofs of the recurrences. Beside establishing the recurrences, our proof combines the formalization of arithmetical ingredients and of some asymptotic analysis. Joint work with Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi.

#### Alain Giorgetti, Richard Genestier and Valerio Senni: *Software Engineering and Enumerative Combinatorics*

We present results on the frontier between two research domains, namely enumerative combinatorics and software engineering, and show how each domain takes profit from the other one.

#### Timothy Gowers: *Fully automatic problem solving with human-style output.*

I shall describe a program that Mohan Ganesalingam and I created that proves simple statements in elementary abstract analysis. I shall also discuss the broader project of which this is intended to be just a preliminary step. Briefly, the aim is to write a series of programs that solve problems in a "fully human" way, meaning that they do not undertake any search that a human mathematician would not consider undertaking. At first, this seems to be sacrificing everything that makes a computer worth using. However, I shall attempt to explain why we regard this view as mistaken

#### Bruno Grenet: *Computing low-degree factors of lacunary polynomials: a Newton-Puiseux approach*

I will present a new polynomial-time algorithm for the computation of the irreducible factors of degree at most d, with multiplicity, of multivariate lacunary polynomials over fields of characteristic zero. The lacunary representation of a polynomial is the list of its nonzero terms, and the size of this representation is in particular logarithmic in the degree of the polynomial. Lacunary polynomials can have factors of exponential size which are therefore not polynomial-time computable, whence the restriction on the degree of the factors that are computed. The algorithm is a deterministic reduction to the computation of irreducible factors of degree at most d of univariate lacunary polynomials on the one hand and to the factorization of low-degree multivariate polynomials on the other hand. The reduction runs in time polynomial in the lacunary size of the input polynomial and in d. As a result, we obtain a new polynomial-time algorithm for the computation of low-degree factors, with multiplicity, of multivariate lacunary polynomials over number fields, but our method also gives partial results for other fields, such as the fields of p-adic numbers or for absolute or approximate factorization for instance. The core of the algorithm uses the Newton polygon of the input polynomial, and its validity is based on the Newton-Puiseux expansion of roots of bivariate polynomials. In particular, we bound the valuation of expressions of expressions of the form f(X,φ) where f is a lacunary polynomial and φ a Puiseux series whose vanishing polynomial has low degree.

#### Alain Herremann: *How to define constructivity? Some few things we can learn from history.*

Turing (1937) offers to set the idea of calculability in arithmetic. Descartes (1637) offers to set the idea of constructibility in geometry. We will compare the two texts and show how and why they are similar in many respects.

#### Philippe Malbos: *Linear rewriting and homology of associative algebras*

We introduce the notion of higher dimensional linear rewriting system for presentations of algebras generalizing the notion of noncommutative Gröbner bases. The aim is twofold, 1/ allow more possibilities of termination orders than those associated to Gröbner bases, only based on monomial orders, 2/ give a description obtained by rewriting of higher syzygies for presentations of algebras. In homological algebra, constructive methods based on noncommutative Gröbner bases were developed to compute projective resolutions by Anick, Green, Berger... In particular, they can be used to study homological properties of associative algebras such as Koszulness. We explain how these constructions fit into the general setting of higher dimensional rewriting theory and how linear rewriting allows more flexibility for the computation of homological properties of associative algebras. This is a joint work with Yves Guiraud and Eric Hoffbeck.

#### Konstantin Mischaikow: *Towards an Algebraic Framework for Nonlinear Dynamics*

The global dynamics of nonlinear systems can exhibit structures over wide varieties of temporal and spatial scales and the same phenomenon is true with respect to parameters. However, from an experimental or computational perspective only a finite amount of information can be collected and measurements can only be made up to a certain level of precision. With this in mind I will argue that we need an alternative description to the qualitative theory of dynamics, preferably based on principles that are easily accessed computationally. I will present some results that represent efforts to develop an algebraic framework for dynamical systems that is based on tools and techniques from combinatorics and algebraic topology.

#### Luca Moci: *Matroids over a ring: motivations, examples, applications.*

Several objects can be associated to a list of vectors with integer coordinates: among others, a family of tori called toric arrangement, a convex polytope called zonotope, a function called vector partition function; these objects have been described in a recent book by De Concini and Procesi. The linear algebra of the list of vectors is axiomatized by the combinatorial notion of a matroid; but several properties of the objects above depend also on the arithmetics of the list. This can be encoded by the notion of a "matroid over Z". Similarly, applications to tropical geometry suggest the introduction of matroids over a discrete valuation ring. Motivated by the examples above, we introduce the more general notion of a "matroid over a commutative ring R". Such a matroid arises for example from a list of elements in a R-module. When R is a Dedekind domain, we can extend the usual properties and operations holding for matroids (e.g., duality). We can also compute the Tutte-Grothendieck ring of matroids over R; the class of a matroid in such a ring specializes to several invariants, such as the Tutte polynomial and the Tutte quasipolynomial. We will also outline other possible applications and open problems. (Joint work with Alex Fink).

#### Anders Mörtberg and Cyril Cohen: *Formalizing elementary divisor rings in Coq*

An elementary divisor ring is a commutative ring where every matrix is equivalent to a matrix in Smith normal form. It is well known that principal ideal domains are elementary divisor rings, but it is an open problem whether the generalization to Bézout domains, rings where every finitely generated ideal is principal, are elementary divisor rings or not. We have formalized, using the Coq proof assistant together with the SSReflect extension, different extension that we can extend Bézout domains with in order to show that they are elementary divisor rings. The extensions we have considered are: existence of a gdco operation, adequacy, Krull dimension less than or equal to 1 and rings where strict divisibility is well-founded.

#### Grant Passmore: *Exact global optimization on demand*

Joint work with Leonardo de Moura of Microsoft Research, Redmond. We present a method for exact global nonlinear optimization based on a real algebraic adaptation of the conflict-driven clause learning (CDCL) approach of modern SAT solving. This method allows polynomial objective functions to be constrained by real algebraic constraint systems with arbitrary boolean structure. Moreover, it can correctly determine when an objective function is unbounded, and can compute exact infima and suprema when they exist. The method requires computations over real closed fields containing infinitesimals (cf. [1]). References: 1. Leonardo de Moura and Grant Olney Passmore. Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. In Proceedings of the 24th International Conference on Automated Deduction (CADE) (2013)

#### Claude Quitté: *Playing with monomials of k[X_1, …, X_n]*

The context is the graded resolution of monomial ideals of k[X_1, …, X_n], where k is a field. The speaker wishes to explain carefully some experiments which led him to understand parts of the correspondance between the monomial world and the simplicial world. In particular : Stanley-Reisner correspondance, various "fine-grading" syzygies formulas (Hochster, Bayer-Charalambous-Popescu), Alexander duality, etc. Tools: algebraic and simplicial Koszul complexes.

#### Christophe Raffalli: *Hilbert's 17th problem via cut-elimination*

Hilbert's seventeen problem, solved by Artin, says that every positive polynomial can be written as a sum of squares of rational fraction. Since Artin, effective proof have been given by Lombardi - Roy - Perrucci for the latest one which give a bound to the degree as a tower of five exponentials. We will see how such a proof can be presented as a result of cut elimination, showing that replacing model theory by proof theory is a possible method to make a result effective. The main contribution of our work is the fact that we implemented the procedure and we introduced a notion of PBDD that requires smaller degrees, making it possible to extract the wanted equalities yet only for the simplest positive polynomials (which was not possible before from such an effective proof).

#### Ana Romero: *Spectral sequences for computing persistent homology*

A filtration of the object to be studied is the heart of both subjects persistent homology and spectral sequences; in the talk I will present the complete relation between them, focusing on constructive and algorithmic points of views. By using some previous programs for computing spectral sequences, we obtain persistent homology programs applicable to spaces not of finite type (provided they are spaces with effective homology) and with Z-coefficients (significantly generalizing the usual presentation of persistent homology over a field).

#### Peter Schuster: *Eliminating Krull's Lemma for Horn Clauses*

Scarpellini [3] has characterised algebraically when in classical logic a certain kind of propositional geometric implication in the language of rings can be proved for commutative rings and for integral domains, respectively. By interpolation, we extend this characterisation to the provability of such implications for reduced rings: that is, commutative rings in which 0 is the only nilpotent element. The characterisation above implies that the theory of integral domains is conservative for Horn clauses over the theory of reduced rings. This allows to eliminate Krull's Lemma for commutative rings from some of the so- called short and elegant proofs in commutative algebra in which the general case is reduced to the special case by reduction modulo a generic prime ideal. The method applies, in particular, to the example studied in [1, 2, 4]: that the non-constant coecients of an invertible polynomial are all nilpotent. 1. Henrik Persson. An application of the constructive spectrum of a ring. In Type Theory and the Integrated Logic of Programs. Chalmers University and University of Goeteborg, 1999. PhD thesis. 2. Fred Richman. Nontrivial uses of trivial rings. Proc. Amer. Math. Soc.,103(4):1012-1014, 1988. 3. Bruno Scarpellini. On the metamathematics of rings and integral domains. Trans. Amer. Math. Soc., 138:71-96, 1969. 4. Peter Schuster. Induction in algebra: a first case study. In 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 581-585. IEEE Computer Society Publications, 2012. Proceedings, LICS 2012, Dubrovnik, Croatia, June 2012. Journal version: Log. Methods Comput. Sci. (3:20) 9 (2013).

#### Francis Sergeraert: *Spectral Sequences downgraded to elementary Gauss Reductions*

The standard Spectral Sequences of Algebraic Topology had been downgraded 25 years ago by Julio Rubio to the Basic Perturbation Lemma, an "elementary" result of homological algebra, in fact relatively complex. The talk is devoted to a reduction of this "lemma" to elementary Gauss reductions, already known by the Babylonians, combined with the invertibility of 1-x when |x| < 1.

#### Bas Spitters: *Constructive algebra and geometric mathematics*

Vickers observed that predicative techniques from formal topology are often preserved under pullbacks of geometric morphisms. This provides a clear technical advantage to such constructions. Constructive algebra, as developed by Coquand and Lombardi provides another important application. I will provide a short overview of some recent such results in analysis, mostly based on our recent article: Bas Spitters, Steven Vickers, and Sander Wolters - Gelfand spectra in Grothendieck toposes using geometric mathematics, 1310.0705, 2013. under revision for QPL 2012 post-proceedings in EPTCS. http://www.cs.ru.nl/~spitters/geoBS.pdf

#### Claire Tête: *Depth, dimension and resolution in Commutative Algebra*

First we introduce two fondamental tools in the theory of depth: the Koszul complex and the Cech complex for a finite sequence (a_1,… ,a_n) in a commutative ring. We give some cohomological properties of these complexes. By using some basic examples, we try to make explicit the links between depth, Krull dimension and resolutions. At the end we illustrate a celebrated Serre theorem characterizing regular rings by existence of finite projective resolutions: we explain THE resolution of the ideal of a point of an hypersurface.

#### Xavier Caruso, David Roe and Tristan Vaccon: *Tracking p-adic precision*

We present a new method to propagate p-adic precision in computations, which also applies to other ultrametric fields. We illustrate it with many examples and give a toy application to the stable computation of the SOMOS 4 sequence. Our methods relies on elementary ultrametric calculus and can either be applied on the fly or as a preparatory step.

#### Marc Giusti and Jean-Claude Yakoubsohn: *Multiplicity hunting and approximating multiple roots of polynomial systems*

The computation of the multiplicity and the approximation of isolated multiple roots of polynomial systems is a difficult problem. In recent years, there has been an increase of activity in this area. Our goal is to translate the theoretical background developed in the last century on the theory of singularities in terms of computation and complexity. This paper presents several different views that are relevant to address the following issues : predict the multiplicity of a root and/or determine the number of roots in a ball, approximate fast a multiple root and give complexity results for such problems. We propose a new method to determine a regular system, called equivalent but deflated, i.e., admitting the same root as the initial singular one. Finally, we perform a numerical analysis of our approach.

#### Noam Zeilberger: *Refining the meaning of types*

Complete the following sequence: * number theorists study numbers * group theorists study groups * knot theorists study knots * type theorists study ___ Many mathematicians would hesitate at giving the obvious answer, because of their inability to explain just what "types" are. Instead they might point to a bunch of different papers where various formal systems are studied, and conclude that "type theorists study type theories". I believe that an important reason for this lack of consensus is that in practice, types are actually used with two very different intuitions in mind, corresponding to the distinction the late John Reynolds termed "intrinsic" versus "extrinsic" [1]. For several years, Paul-André Melliès and I have been developing a category-theoretic approach to type theory that aims to reconcile these two opposing intuitions, the essence of which may be explained by the following simple idea: just as any category may be viewed (à la Lambek) as a deductive system (supporting composition of deductions), any *functor* may be viewed as a type system (supporting composition of typing derivations). Our approach is closely related to (and partly inspired by) an idea which appears in the type-theoretic literature under the heading of "refinement", developed especially by Frank Pfenning and his students. In the talk, I will begin by giving a partial survey of the work on type refinement and some of the practical motivations behind it. Then I will introduce our abstract definition of a type (refinement) system, and describe various ways it can be used. 1. John C. Reynolds, "The Meaning of Types -- From Intrinsic to Extrinsic Semantics", BRICS Report Series RS-00-32, December 2000. Available from http://www.brics.dk/RS/00/32/