Program

Monday 26

9:30 - 10:00Welcome
10:00 - 11:00Claire TêteInvited tutorial: Depth, dimension and resolution in Commutative Algebra
30min break
11:30 - 12:30Alain HerremannInvited talk: How to define constructivity? Some few things we can learn from history.
lunch break (1h45)
14:15 - 15:15Claude QuittéInvited talk: Playing with monomials of k[X_1, …, X_n]
15:15 - 16:15Konstantin MischaikowInvited tutorial: Towards an Algebraic Framework for Nonlinear Dynamics
45min break
17:00 - 18:00Timothy GowersExternal event: Fully automatic problem solving with human-style output.

Tuesday 27

9:00 - 10:00Claire TêteInvited tutorial: Depth, dimension and resolution in Commutative Algebra
10:00 - 10:30Francis SergeraertContributed talk: Spectral Sequences downgraded to elementary Gauss Reductions
30min break
11:00 - 12:00Frédéric ChyzakInvited talk: A Computer-Algebra-Based Formal Proof of the Irrationality of ζ(3)
12:00 - 12:30Anders Mörtberg and Cyril CohenContributed talk: Formalizing elementary divisor rings in Coq
lunch break (1h45)
14:15 - 15:15Noam ZeilbergerInvited talk: Refining the meaning of types
15:15 - 15:45Xavier Caruso, David Roe and Tristan VacconContributed talk: Tracking p-adic precision
15:45 - 16:15MAP meeting
EveningMAP dinner

Wednesday 28

9:00 - 10:00Konstantin MischaikowInvited tutorial: Towards an Algebraic Framework for Nonlinear Dynamics
10:00 - 10:30Marc Giusti and Jean-Claude YakoubsohnContributed talk: Multiplicity hunting and approximating multiple roots of polynomial systems
30min break
11:00 - 12:00Luca MociInvited talk: Matroids over a ring: motivations, examples, applications.
12:00 - 12:30Alain Giorgetti, Richard Genestier and Valerio SenniContributed talk: Software Engineering and Enumerative Combinatorics
lunch break (1h45)
14:15 - 15:15Christophe RaffalliInvited talk: Hilbert's 17th problem via cut-elimination
15:15 - 16:15Claire TêteInvited tutorial: Depth, dimension and resolution in Commutative Algebra

Thursday 29 is a French holiday.

Friday 30

9:00 - 10:00Konstantin MischaikowInvited tutorial: Towards an Algebraic Framework for Nonlinear Dynamics
10:00 - 10:30Peter SchusterContributed talk: Eliminating Krull's Lemma for Horn Clauses
30min break
11:00 - 12:00Ana RomeroInvited talk: Spectral sequences for computing persistent homology
12:00 - 12:30Philippe MalbosContributed talk: Linear rewriting and homology of associative algebras
lunch break (1h45)
14:15 - 15:15Grant PassmoreInvited talk: Exact global optimization on demand
15:15 - 15:45Bas SpittersContributed talk: Constructive algebra and geometric mathematics
15:45 - 16:15Bruno GrenetContributed 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)

Slides
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

Slides
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

Slides
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

Slides first tutorial
Slides second tutorial
Slides third tutorial
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.

Slides
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

Slides
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

Slides
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

Slides
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

Slides
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

Slides
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

Slides first tutorial
Slides second tutorial
Slides third tutorial
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

Slides
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

Slides
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

Slides
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/