The University of Adelaide
You are here » Home » News and events
Text size: S | M | L
Printer Friendly Version
November 2018

Events on Friday 05 October 2018

Exceptional quantum symmetries
11:10 Fri 5 Oct, 2018 :: Barr Smith South Polygon Lecture theatre :: Scott Morrison :: Australian National University

I will survey our current understanding of "quantum symmetries", the mathematical models of topological order, in particular through the formalism of fusion categories. Our very limited classification results to date point to nearly all examples being built out of data coming from finite groups, quantum groups at roots of unity, and cohomological data. However, there are a small number of "exceptional" quantum symmetries that so far appear to be disconnected from the world of classical symmetries as studied in representation theory and group theory. I'll give an update on recent progress understanding these examples.
Interactive theorem proving for mathematicians
15:10 Fri 5 Oct, 2018 :: Napier 208 :: A/Prof Scott Morrison :: Australian National University

Mathematicians use computers to write their proofs (LaTeX), and to do their calculations (Sage, Mathematica, Maple, Matlab, etc, as well as custom code for simulations or searches). However today we rarely use computers to help us to construct and understand proofs. There is a long tradition in computer science of interactive and automatic theorem proving; particularly today these are important tools in engineering correct software, as well as in optimisation and compilation. There have been some notable examples of formalisation of modern mathematics (e.g. the odd order theorem, the Kepler conjecture, and the four-colour theorem). Even in these cases, huge engineering efforts were required to translate the mathematics to a form a computer could understand. Moreover, in most areas of research there is a huge gap between the interests of human mathematicians and the abilities of computer provers. Nevertheless, I think it's time for mathematicians to start getting interested in interactive theorem provers! It's now possible to write proofs, and write tools that help write proofs, in languages which are expressive enough to encompass most of modern mathematics, and ergonomic enough to use for general purpose programming. I'll give an informal introduction to dependent type theory (the logical foundation of many modern theorem provers), some examples of doing mathematics in such a system, and my experiences working with mathematics students in these systems.
Recent news
Further enquiries

School of
Mathematical Sciences

Levels 6 and 7
Ingkarni Wardli Building
North Terrace Campus
The University of Adelaide
SA 5005 Australia

See location on map

General email
Head of School email
Telephone: +61 8 8313 5407
Facsimile: +61 8 8313 3696