The seminar is held in Room 107 of Peter Hall. For announcements of talks subscribe to the mailing list. The videos from the talks are available on YouTube. For previous semesters of the seminar, scroll down! In semester two of 2019 we are going to study reasoning in the context of **deep reinforcement learning** with an aim to understand AlphaGo and related breakthroughs, such as AlphaStar. Along the way we will look at deep learning more generally. Some relevant background information:

AlphaGo documentary on NetFlix.

Deep RL for theorem proving an interview with Szegedy.

There are three main components of AlphaGo: *Monte-Carlo tree search*, *deep learning* and *reinforcement learning*, and we will have talks on all three aspects. One important running theme will be the dichotomy between problems with small and large state spaces, and the corresponding need for function approximation (the successful incorporation of which is what makes AlphaGo scientifically interesting).

Talk schedule:

- Lecture 1: Daniel Murfet “Introduction to reinforcement learning” (notes) (Bellman equation)
- Lecture 2: James Clift “Turing and Intelligent Machinery” (paper)
- Lecture 3: Thomas Quella “Hopfield networks and statistical mechanics”
- Lecture 4: Will Troiani “Universal approximation by feedforward networks” (ref also constructively) (counter-examples ala Minsky)
- Lecture 5: Susan Wei “An introduction to deep learning” (autodiff, optimisation alg SGD, initialisations)
- Lecture 6: ??? “Convolutional networks and deep reinforcement learning” (Sutton & Barto)
- Lecture 7: James Clift “Solving games with tree search” (
*alpha-beta search*,*dynamic programming*) - Lecture 8: Daniel Murfet “AlphaGo” (following the DeepMind paper, also Sutton & Barto)
- Lecture 9: Daniel Murfet “AlphaStar and attention”

Currently unscheduled talks:

- Lecture ??: Rohan Mitta “Theorem proving and Lean”
- Lecture ??: Elliot Catt “Solomonoff induction and the limits of RL”

Background on deep learning and reinforcement learning:

- I. Goodfellow, Y. Bengio, A. Courville “Deep learning“
- R. S. Sutton and A. G. Barto “Reinforcement learning” 2nd edition, 2018.
- C. F. Higham, D. J. Higham “Deep learning: an introduction for applied mathematicians“
- F. Chollet “Deep learning with Python” (practical)

**UPDATE:** The seminar webpage has moved here.

The aim of the seminar in semester one of 2019 is to understand **topological error correcting codes and how they enable universal quantum computers**. This is a remarkable application of topology to computation: one promising approach to making quantum computing work in practice is based on the homology and cohomology of surfaces. Moreover, some of our neighbours are at the forefront of building quantum computers based on these ideas. An attractive feature of the subject is the sheer boldness of the underlying ideas, for example in Deutsch’s paper on universal quantum computation he writes in a section titled “Programming physics”:

To view the Church-Turing hypothesis as a physical principle does not merely make computer science a branch of physics. It also makes part of experimental physics into a branch of computer science. The existence of a universal quantum computer Q implies that there exists a program for each physical process.

For an entree to quantum computing, see the following recent talks:

- 2018 Australian of the Year Michelle Simmons “The Einstein Lecture: The Quantum Computing Revolution” (material on implementations of error correction from about 49:00).
- Jason Alicea “Topological Quantum Computing: Plenty of Room in the Middle” 2018.

Preliminary talks (preceding the semester):

- Lecture A: James Clift “Universal Turing Machines”
- Lecture B: Will Troiani “Reversible Turing Machines”

Talk schedule (beginning week 1):

- Lecture 1: Daniel Murfet “Introduction to the seminar”
- Lecture 2: Thomas Quella “Crash course in quantum mechanics”
- Lecture 3: Isaac David Smith “Feynman’s quantum circuits”
- Lecture 4: Will Troiani “Deutsch’s universal quantum computer (Part 1)”
- Lecture 5: Daniel Murfet “Deutsch’s universal quantum computer (Part 2)”
- Lecture 6: TBD “Applications of quantum computers”
- Lecture 7: Thomas Quella “Physical realisations of quantum computers”
- Lecture 8: James Clift “Classical error correcting codes and multiplexing” (notes)
- Lecture 9: Will Troiani “Crash course in homology and cohomology”
- Lecture 10: Isaac David Smith “Topological error correcting codes (Part 1)” (notes)
- Lecture 11: Isaac David Smith “Topological error correcting codes (Part 2)” (notes)
- Lecture 12: Thomas Quella “Tensor networks and quantum computation”
- Lecture 13: Charles Hill “Open problems for mathematicians”

Primary references:

- [AB] S. Arora, B. Barak “Computational complexity” 2009
- [B] C. H. Bennett “Logical reversibility of computation” 1973
- [F] R. Feynman “Lectures on Computation” 1996.
- [D] D. Deutsch, “Quantum theory, the Church-Turing principle and the quantum computer” 1985.
- [DKLP] E. Dennis, A. Kitaev, A. Landahl, J. Preskill “Topological quantum memory” 2001
- [K] A. Kitaev “Fault-tolerant quantum computation by anyons” 2003.
- [C] C. Hill, E. Peretez, S. J. Hile, M. G. House, M. Fuechsle, S. Rogge, M. Y. Simmons and L. C. L. Hollenberg “A surface code quantum computer in silicon” 2015
- [NC] M. Nielsen, I. Chuang “Quantum computation and quantum information” 2010.

Explanation of the talk schedule: the aim by the end of the semester is to understand what a universal quantum computer is [D] and how the surface code introduced in [DKLP] and elaborated in [C] solves the main problem that one faces in actually physically realising such a computer, namely, quantum error correction. To understand what a universal quantum computer is, one has to first know what universal computation means (hence, Universal Turing Machines) and what reversible computation means, and to understand quantum error correction it is important to have seen classical error correction.

Other useful links:

- D. Brown, “Lectures on topological codes and quantum computation“
- National Academies of Sciences, Engineering, and Medicine “Quantum Computing: Progress and Prospects” 2018.

Our aim in the second semester of 2018 was to understand **how to use adjoint functors and topoi to organise mathematical knowledge**, following Mac Lane and Moerdijk’s book “Sheaves in Geometry and Logic”. For an explanation of this aim see the seminar announcement and the first lecture below. The seminar is supported by funding from Data61, DST group and ACEMS as part of a collaboration which aims to develop new tools to aid human reasoning about mathematics and software.

Talk schedule:

- Lecture 1: Daniel Murfet “An invitation to topos theory” (notes | video)
- Lecture 2: Daniel Murfet “The Curry-Howard correspondence (Part 1)” (notes | video | more notes | response to Sam’s question)
- Lecture 3: Will Troiani “Monads and programs” (notes | video)
- Lecture 4: James Clift “The definition of a topos (Part 1)” (notes | video)
- Lecture 5: James Clift “The definition of a topos (Part 2)” (notes | video)
- Lecture 6: Patrick Elliott “Sheaves of sets (Part 1)” (notes | video)
- Lecture 7: Patrick Elliott “Sheaves of sets (Part 2)” (notes | video)
- Lecture 8: Will Troiani “Higher-order logic and topoi (Part 1)” (notes | video)
- Lecture 9: Daniel Murfet “Higher-order logic and topoi (Part 2)” (notes | video)
- Lecture 10: Patrick Elliott “Sheaves form a topos (Part 1)” (notes | video)
- Lecture 11: Patrick Elliott “Sheaves form a topos (Part 2)” (notes | video)
- Lecture 12: Daniel Murfet “Classifying topoi (Part 1)” (notes | video)
- Lecture 13: James Clift “Higher-order logic and topoi (Part 3)” (notes | video)
- Lecture 14: Will Troiani “The classifying space of rings” (notes)
- Lecture 15: Daniel Murfet “Abstraction and adjunction” (notes | video1)

References:

- Mac lane, Moerdijk “Sheaves in Geometry and Logic”.
- Lambek, Scott “Introduction to higher-order categorical logic”
- Barr, Wells “Toposes, triples and theories”
- Sorensen, Urzyczyn “Lectures on the Curry-Howard isomorphism”.
- Caramello’s paper “The unification of mathematics via topos theory”,
- Cartier’s paper “A mad day’s work: from Grothendieck to Connes and Kontsevich”,
- Higher topoi are important in homotopy type theory,
- Connes’ talk on “The arithmetic site”.

Our aim was to read Sorensen and Urzyczyn’s book “Lectures on the Curry-Howard isomorphism”, up to the proof of the original Curry-Howard correspondence (between simply-typed lambda calculus and intuitionistic logic) in Chapter 4.

- 14-7 William Troiani “The Church-Rosser Theorem” (lecture notes)
- 2-8 William Troiani “Introduction to lambda calculus” (Sections 1.1-1.3, lecture notes)
- 9-8 Samuel Lyons “All partial recursive functions are lambda-definable” (Section 1.7, lecture notes)
- 16-8 James Clift “Simply-typed lambda calculus and strong normalisation” (Chapter 3, lecture notes)
- 23-8 Shawn Standefer “Introduction to natural deduction” (Chapter 2, lecture notes)
- 30-8 Daniel Murfet “The category of simply-typed lambda terms” (lecture notes)
- 6-9 Shawn Standefer “Kripke semantics of intuitionistic logic” (lecture notes)
- 13-9
**No talk**, instead we’ll watch Wadler’s Propositions as types and discuss - 20-9 Daniel Murfet “The category of simply-typed lambda terms II” (lecture notes and an appendix)
- 4-10 Daniel Murfet “The Curry-Howard principle” (lecture notes)
- 11-10 James Clift “System F: Polymorphic lambda calculus” (lecture notes)
- 18-10 William Troiani “System F in the real world: Haskell and functional programming” (lecture notes) (the referenced talk by Rich Hickey is “Simple made easy”)

References:

- Sorensen, Urzyczyn “Lectures on the Curry-Howard isomorphism”.
- Girard, Lafont, Taylor “Proofs and types”.
- Gallier “Constructive Logics Part I”.
- Wadler “Propositions as types”.
- Martin-Lof “On the meanings of the logical constants and the justifications of the logical laws”.

Our aim was to read Kock’s book on the equivalence between closed 2D TFTs and commutative Frobenius algebras. The talks:

- 28-7 Daniel Murfet “Topological Quantum Field Theory in two dimensions” (slides).
- 4-8 Patrick Elliott “Introduction to Frobenius algebras” (lecture notes).
- 11-8 Michelle Strumila “The cobordism category 2Cob” (beginning of Chapter 1, lecture notes).
- 18-8 Omar Foda “Supersymmetry and Morse theory” (references are Witten’s paper and Nicolas Mee’s thesis).
- 1-9 Patrick Elliott “The category of Frobenius algebras” (lecture notes).
- 8-9 Thomas Quella “Chern-Simons theory as an example of a TQFT” (lecture notes).
- 15-9 Campbell Wheeler “Symmetric monoidal categories and functors” (lecture notes).
- 13-10 Daniel Murfet “The cobordism category” (lecture notes).

References:

- [K] J. Kock’s TQFT book.
- [Ks] J. Kock’s short version of the TQFT book.
- Atiyah “An introduction to Topological Quantum Field Theories“
- Atiyah “Topological quantum field theories” Publications Mathematiques de l’IHES, 68 (1988), p. 175-186.
- Segal “The definition of conformal field theory“
- Lurie “On the classification of topological field theories“
- Carqueville “Lecture notes on 2-dimensional defect TFT” (2016).
- Carqueville “3-dimensional defect TQFTs and their tricategories” (2016).
- Kapustin “Topological Field Theory, Higher Categories, and Their Applications” (2010).