Program
Monday 26
Tuesday 27
Wednesday 28
Thursday 29 is a French holiday.
Friday 30
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/