Abstracts

Title: A heuristic prover for real inequalities (joint work with Robert Y. Lewis and Cody Roux)
Abstract: We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem proving. In contrast to approaches that aim to be complete with respect to a particular language or class of formulas, our method establishes claims that require heterogeneous forms of reasoning, relying on a Nelson-Oppen-style architecture in which special-purpose modules collaborate and share information. The framework is thus modular and extensible. A prototype implementation shows that the method works well on a variety of examples, and complements techniques that are used by contemporary interactive provers.
Speaker: Jon Borwein
Title: Short walks in higher dimensions
Abstract: We study arithmetic properties of short uniform random walks in arbitrary dimensions, with a focus on explicit (hypergeometric) evaluations of the moment functions and probability densities in the case of up to five steps. Somewhat to our surprise, we are able to provide complete extensions to arbitrary dimensions for most of the central results known in the two dimensional case.
Speaker: Richard Brent
Title: Asymptotics of some functions arising in number theory and analysis of algorithms via computation and Mellin transforms
Abstract: We consider the asymptotic behaviour of some interesting functions that arise naturally in the analysis of algorithms (for example, analysis of the average behaviour of the binary Euclidean algorithm) and in number theory (for example, in proving algebraic independence results using Mahler's method). The asymptotic behaviour of these functions was first explored via computation and later explained via Mellin transforms.
Speaker: Cris Calude
Title: Proving quantum indeterminism: Measurements of value indefinite observables are unpredictable
Abstract: We prove that quantum indeterminism — formally modelled as value indefiniteness — is incompatible with the supposition of predictability: measurements of value indefinite observables are unpredictable. The proof makes essential use of a strengthened form of the Kochen-Specker theorem and relies on three assumptions: compatibility with quantum mechanical predictions, non-contextuality, and the value definiteness of observables corresponding to the preparation basis of a quantum state.
Speaker: John Cannon
Title: The Classification Theorem for Finite Simple Groups as a Basis for Algorithms for Finite Groups.
Abstract: Group theory has proved to be fertile ground for constructing algorithms with a large number of useful algorithms for computing structural information being published over the past 55 years. Soon after the CTFSG was announced in 1983, researchers started thinking about how the CTFSG could be used to produce more powerful algorithms. In this talk I will outline a major international project currently under way that uses the CTFSG to reduce computations in a large group down to calculations with its (simple) composition factors. This approach is opening up the possibility of doing structural computation with finite matrix groups having degrees in the 1000s.
Speaker: Attila Egri-Nagy
Title: Extending the computational horizon
Abstract: For studying finite structures it is helpful to generate small examples by computer programs. By investigating these sample objects we can formulate new hypotheses and falsify conjectures by counterexamples. At a given time, the available computing power and the state of the art algorithms define a limit on the size of the examples we can investigate. This limit we call the computational horizon, similar to the cosmological horizon determined by the size of our observable physical universe. The underlying assumption in both fields is that we can see enough within our limits to enable us to go beyond by theoretical reasoning, i.e. to have enough observational data to construct valid theories. In this talk we describe how computer calculations advanced our understanding of bacterial genomics and the foundations of computing.
Speaker: Murray Elder
Title: Computational problems in infinite groups
Abstract: I will describe my recent work on two major problems in infinite group theory — first, the problem of deciding whether an equation in a free group has a solution, finding all solutions, and describing all solutions in a computationally efficient way, and second, the question of amenability for certain groups, in particular Richard Thompson's group $F$. In the first case, with Laura Ciobanu and Volker Diekert, we prove that the set of all solutions to an equation is a Lindenmayer language of type EDT0L. We construct this formal language description in quasilinear space in the size of the input equation. In the second case, with Andrew Rechnitzer and Buks van Rensburg, we apply techniques from statistical mechanics to experimentally decide amenability in a range of groups.

Speaker: John Harrison
Title: Experimental computations related to the asymptotic behaviour of random walks on certain matrix groups
Abstract: Random walks have been used to model stochastic processes in many scientific fields. I will introduce invariant random walks on groups, where the transition probabilities are given by a probability measure. The Poisson boundary will also be discussed. It is a space associated with every group random walk that encapsulates the behaviour of the walks at infinity. I will then discuss my attempts to describe the boundary for a certain family of matrix groups with particular emphasis on the various ways that computer experiments have aided my progress.
Speaker: Rob Lewis
Title: Dependent types and the algebraic hierarchy
Abstract: A proof assistant for mathematics should recognize relationships been algebraic structures and instances; for example, that every semigroup is a group, a ring extends both an additive group and a multiplicative monoid, and the integers are an instance of an ordered ring. Managing these relationships makes it possible to use definitions, theorems, and notation developed for semigroups, for example, when reasoning about arbitrary rings, and the integers in particular.

We describe a way of accomplishing this, implemented in the Lean theorem prover. Lean is based on dependent type theory, and expressive foundational language in which every object has an associated "type". Lean supports a mechanism known as type class inference , which was originally designed to support generic programming in functional programming languages. I will explain how dependent type theory and type classes are ideally suited to managing the algebraic hierarchy as well.

Speaker: Pablo Moscato
Title: Using Evolution and L-systems for Intelligent Design and other attempts to narrow the gap between Theory and Practice in Computer Science
Abstract: We present a heuristic technique for analysing an algorithm by means of searching for input instances which cause the program to run in its worst-case time. The method is discussed within the context of lack of advances in the study of NP-hard optimisation problems.

Concorde is the state-of-the-art Traveling Salesperson Problem (TSP) solver, and is based on evolutionary computation techniques (i.e. it can be classified as an anytime complete memetic algorithm which uses multiparent-recombination).

We have used Concorde to test our approach. We seed our .evolutionary attack. with a fractal instance of the TSP, defined by a Lindenmayer system at a fixed order. The evolutionary algorithm produced modifications to the L-System rules such that the instances of the modified L-System become increasingly much harder for Concorde to solve to optimality. In some cases, while still having the same size, the evolved instances required a computation time which was 30,000 times greater than what was needed to solve the original instance that seeded the search. The success of this case study shows the potential of Evolutionary Search to provide new test-case scenarios for algorithms and their software implementations.

We discuss these results within the context of the .Hard Puzzle Conjecture., the lack of progress of approximability as a guiding theory in Computer Science, and the unreasonable gap between Theory and Practice.

Keywords: Evolutionary Analysis of Algorithms, Man-Machine Memetic Design, fractals, L-Systems

Speaker: Michael Rose
Title: Expectations over Fractal Sets
Abstract: In a previous work, the authors extended the classical notion of box integrals - expectations over unit hypercubes - to encompass a class of Cantor-like fractal sets. We present a generalisation of this work in which the definition of expectation is extended to any smooth complex-valued function defined over the fractal attractor of an iterated function system. Our main result is a self-similarity relation for such expectations that facilitates their symbolic computation in certain cases.
Speaker: Matt Skerritt
Title: On the use of GPU's in Mathematical Computation
Abstract: The use of GPUs for scientific computation has undergone phenomenal growth over the past decade, as hardware originally designed with limited instruction sets for image generation and processing has become fully programmable and massively parallel. This talk discusses the classes of problem that can be attacked with such tools, as well as some practical aspects of implementation.
Speaker: Matthew Tam
Title: Reconstruction Algorithms in Blind Ptychographic Imaging
Abstract: In scanning ptychography, an unknown specimen is illuminated by a localized illumination function resulting in an exit-wave whose intensity is observed in the far-field. A ptychography dataset is a series of these observations, each of which is obtained by shifting the illumination function to a different position relative to the specimen, with neighbouring illumination regions overlapping. Given a ptychographic dataset, the blind ptychography problem is to simultaneously reconstruct the specimen, illumination function, and relative phase of the exit-wave. In this talk I will discuss a framework which recovers current state-of-the-art ptychography algorithms as limiting cases whilst provides further flexibility. (Joint work with R. Hesse, D.R. Luke, and S. Sabach)
Speaker: Don Taylor
Title: Janko's sporadic simple groups: a bit of history
Abstract: Fifty years ago, to quote George Szekeres, "Australian mathematics produced something which surprised the whole world": Zvonimir Janko, working at the ANU, discovered and constructed a new simple group which was neither an alternating group nor a group of Lie type. A decade later the number of new sporadic simple groups had risen to 21 and Janko had found four of them, including the first and the last. This talk recounts some of the history of those exciting times.
Title: On a family of polynomials related to $\zeta(2,1) = \zeta(3)$