* Dates within the next 7 days are marked by a star.
Niklas Halonen (University of Helsinki)
Automated Grading in Lean Using Comparator
* Today * Friday 02 October 2026, 13:15, U4062, University of Helsinki main building (Fabianinkatu 33)
In my talk, I give an introduction to Comparator and briefly explain the principles and challenges behind it. I will also demonstrate my tool for automated grading of Lean exercises called "comparator-autograder".
Aalto-Helsinki formalized mathematics seminar
Vanni Noferini (Aalto)
Rosenbrock's Theorem characterizes Prüfer domains
* Monday 05 October 2026, 14:15, M3 (M234)
Under coprimality assumptions on certain submatrices, Rosenbrock's Theorem relates the invariant factors of a matrix P to those of its "transfer function" (an engineering term that denotes the Schur complement of a leading principal submatrix, assumed invertible) G. Motivated by applications in systems theory, Rosenbrock first proved this result in the 1960s for P \in \R[x]. In 1974, Coppel proved Rosenbrock's Theorem in much broader generality, assuming that the base ring is a PID.
I would like to discuss some recent results on this theorem:
Even Coppel's assumptions can be weakened further to show that Rosenbrock's Theorem holds over any elementary divisor domain (EDD). This is relevant for engineering applications over the ring of entire functions. Moreover, even when the assumptions of the theorem do not hold, it is possible to estimate the relation between the invariant factors of P and G.
Because the Smith and Smith-McMIllan forms are only guaranteed to exist over an EDD (or its field of fractions), the result in part (a) means that Rosenbrock's Theorem holds for every integral domain over which its original statement makes sense. However, it possible to reopen the question by translating the statement in the language of fractional ideals. One can then prove that this "ideal-theoretic Rosenbrock's Theorem" holds if and only if the underlying ring is a Prüfer domain. For more general rings, several interesting partial results can also be stated, some of which are still motivated by applications to engineering. Some connections with the Quillen-Suslin theorem also arise.
Part (a) is based on joint work with Dopico and Zaballa; part (b) is based on a single authored paper.
AGC Seminar
Aleksis Koski
The Radó-Kneser-Choquet Theorem Revisited
* Wednesday 07 October 2026, 10:15, M3 (M234)
The Radó-Kneser-Choquet Theorem is a beautiful classical result about harmonic mappings in the plane. It has many fundamental applications in modern nonlinear elasticity. The theorem has two quite distinct proofs, one classical and one more modern. In this talk, we will discuss a third proof idea, with surprising consequences.
Thanh-Long Tran (University of Helsinki)
TBA
Friday 09 October 2026, 13:15, U4062, University of Helsinki main building (Fabianinkatu 33)
Aalto-Helsinki formalized mathematics seminar
Prof. Lenny Fukshansky (Claremont McKenna College)
Two algebraic contructions of structured lattices
Thursday 15 October 2026, 14:15, M3 (M234)
We discuss two algebraic constructions of lattices with special geometric properties. First, we consider free Z-modules spanned by algebraic conjugates of some algebraic numbers under Minkowski embedding into a Euclidean space. We are interested in conditions on the corresponding algebraic numbers that results in well-rounded nearly-orthogonal lattices with large automorophism groups. Second, we consider lattices generated by orbits of a single vector under permutation by a fixed element of the symmetric group. We show that such lattices have a great deal of structure and posess some interesting properties. One example of such lattices comes from free Z-modules in number fields and is related to the first construction.
ANTA Seminar / Hollanti et al.
Kristian Latvanen (Aalto University)
Formalizing percolation
Friday 16 October 2026, 13:15, U4062, University of Helsinki main building (Fabianinkatu 33)
I will describe our current project on formalizing percolation theory, more specifically, sharpness of percolation phase transition. Due to advances in AI, the emphasis of the project has shifted somewhat, most recently due to a full LLM-generated formalization of the original goal by Anthropic. Especially, I will describe what has been learned in writing a Mathlib-quality version of the result and the usefulness of LLMs in it.
Aalto-Helsinki formalized mathematics seminar
Ragnar Freij-Hollanti (Aalto)
TBA
Monday 19 October 2026, 14:15, M3 (M234)
TBA
AGC Seminar
Waltteri Keus
TBA (Master's thesis presentation)
Tuesday 20 October 2026, 11:00, M2 (M233)
TBA
Aalto Stochastics and Statistics Seminar / Tölle
Henri Lahdelma
Midterm review talk
Wednesday 21 October 2026, 10:15, M3 (M234)
Analysis seminar
Anna-Mariya Otsetova
TBA
Wednesday 21 October 2026, 11:15, M3 (M234)
Analysis seminar
Dr. Razane Tajeddine
TBA
Thursday 22 October 2026, 14:15, M3 (M234)
ANTA Seminar / Hollanti et al.
Prof. Marcus Greferath (University College Dublin/Aalto)
On my recent work on noiseless and noisy group testing (Part II)
Thursday 22 October 2026, 14:15, M3 (M234)
Group testing is a branch of the mathematics of communications and coding theory that is almost as old as Shannon's information theory itself. It arose from the need to screen populations of potentially infected individuals for an infectious disease with as few tests as possible, since testing was expensive or otherwise cumbersome. Current developments in the field assume that tests may be considerably cheaper but are often affected by false positives and false negatives. This reopens the line of research known as error-correcting group testing. In this talk, we revisit several old and new ideas in the language of residuation theory and show how this framework mitigates some of the awkwardness of earlier approaches to modelling the problem. We conclude the presentation with results on the error tolerance and test efficiency of various examples of error-correcting group testing schemes based on finite geometries, partial linear spaces, and other appealing combinatorial designs.
Remark: This talk is dedicated to my late wife, Cornelia Roessing, who encouraged me to take up this awarding field within the mathematics of communications. It includes joint work with Oliver Gnilke (Aalborg), Johan Dinesen (Aalto), and David Forbes (UCD).
ANTA Seminar / Hollanti et al.
Prof. Marcus Greferath (University College Dublin/Aalto)
On my recent work on noiseless and noisy group testing (Part II)
Thursday 29 October 2026, 15:15, M3 (M234)
Group testing is a branch of the mathematics of communications and coding theory that is almost as old as Shannon's information theory itself. It arose from the need to screen populations of potentially infected individuals for an infectious disease with as few tests as possible, since testing was expensive or otherwise cumbersome. Current developments in the field assume that tests may be considerably cheaper but are often affected by false positives and false negatives. This reopens the line of research known as error-correcting group testing. In this talk, we revisit several old and new ideas in the language of residuation theory and show how this framework mitigates some of the awkwardness of earlier approaches to modelling the problem. We conclude the presentation with results on the error tolerance and test efficiency of various examples of error-correcting group testing schemes based on finite geometries, partial linear spaces, and other appealing combinatorial designs.
Remark: This talk is dedicated to my late wife, Cornelia Roessing, who encouraged me to take up this awarding field within the mathematics of communications. It includes joint work with Oliver Gnilke (Aalborg), Johan Dinesen (Aalto), and David Forbes (UCD).
ANTA Seminar / Hollanti et al.
Wontae Kim (Korea Institute for Advanced Study)
TBA
Wednesday 04 November 2026, 10:15, M3 (M234)
Analysis seminar
Andrea Fornetto
Locally recoverable codes for data storage: constructions via elliptic curves and surfaces
Thursday 12 November 2026, 14:15, M3 (M234)
ANTA Seminar / Hollanti et al.
Show the events of the past year
Page content by: webmaster-math [at] list [dot] aalto [dot] fi