* Dates within the next 7 days are marked by a star.
Niklas Halonen
Computer Formalization of the Real Numbers in Lean 4
* Today * Thursday 28 August 2025, 16:15, M2 (M233)
I will introduce a construction of the (Cauchy) reals using quotient types in the Lean 4 theorem prover, as well as formalization tools like linarith, ring, the simplifier simp, its augmentation, and metaprogramming with custom tactics. The approach is based on Riccardo Brasca's (Real) Numbers game. For an in-depth documentation about Lean's quotient types, see: https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Computation/ and https://lean-lang.org/doc/reference/latest/The-Type-System/Quotients/
Dr. Padraig Ó Catháin
Monomial groups and combinatorial matrices
Thursday 11 September 2025, 15:15, M3 (M234)
D. G. Higman observed that the centraliser algebra of a rank 3 permutation group is spanned by the incidence matrix of a strongly regular graph on which the permutation group acts by automorphisms. Quite generally, incidence matrices of combinatorial structures invariant under a permutation group are contained in the centraliser algebra of the corresponding permutation representation.
In this talk, I will explain how monomial representations act on matrices of combinatorial interest with entries in a finite subset of $\mathbb{C}$. I will explain how central extensions, character sums and Gröbner basis techniques can be combined to classify complex Hadamard matrices with sufficiently rich automorphism groups. The talk will require knowledge only of elementary group theory and linear algebra. This is joint work with Santiago Barrera-Acevedo, Heiko Dietrich and Ronan Egan.
ANTA Seminar / Hollanti et al.
Show the events of the past year
Page content by: webmaster-math [at] list [dot] aalto [dot] fi