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.

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.

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.

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.

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.

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.

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.

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.

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.

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

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.

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.

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)

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.

Abstract: We outline a new proof of an identity of the multiple zeta values that generalizes the classical one from the title, using generating functions of the underlying generalized polylogarithms and symbolic algorithms of hypergeometric functions. A new family of (hypergeometric) polynomials that shows up in the proof satisfies 3-term recurrence relations and has several remarkable analytical properties. We also indicate experimental observations about a similar-generated family of polynomials for an (ex-)conjectural identity of Borwein, Bradley and Broadhurst.