A few years ago, the idea of formalising modern research level mathematics seemed completely out of reach. Since then, more and more examples have appeared. I'll go through several examples (some related to the mathematics of Scholze, Tao and Gowers), and talk about how the process is evolving, enabling multiple people to collaborate in the formalisation of modern research in real time. Computer-verified proofs: 48 hours in Rome

In this talk I will describe what goes on behind the scenes of Lean. I will explain the logic of Lean, called dependent type theory, what Lean tactics are and explain why we can trust proofs that are checked by Lean. Computer-verified proofs: 48 hours in Rome

This presentation will explore the pivotal role of the Lean in enhancing first-year undergraduates' understanding of mathematical proofs. I will share insights from my experiences and initial educational research on teaching a large first-year undergraduate cohort with Lean, focusing on how this tool can significantly impact student perception of proofs. Additionally, I will address the challenges encountered in teaching with Lean and the implications for learning and comprehension. Computer-verified proofs: 48 hours in Rome

In this talk I will illustrate how certain programs, of which Lean is an example, permit to interact with a computer about the logical soundness of mathematical arguments. I will go through the details of well-known proofs trying to understand the feedback provided by the computer and will try to share the fun involved in the process. Computer-verified proofs: 48 hours in Rome

We call internal-wave billiard the dynamical system of a point particle that moves freely inside a planar domain (the table) and is reflected by its boundary according to this rule: reflections are standard Fresnel reflections but with the pretense that the boundary at any collision point is either horizontal or vertical (relative to a predetermined direction representing gravity). These systems are point particle approximations for the motion of internal gravity waves in closed containers, hence the name. The phenomenon of internal waves in a fluid occurs in many situations and has been intensively studied by physicists. One of the first experiments, which became paradigmatic, was done in a container shaped like a rectangular trapezoid (with some thickness). For a class of tables including rectangular trapezoids, we prove that the dynamics has only three asymptotic regimes: (1) there exist a global attractor and a global repellor, which are periodic and might coincide; (2) there exists a beam of periodic trajectories, whose boundary (if any) comprises an attractor and a repellor for all the other trajectories; (3) all trajectories are dense (that is, the system is minimal). If time permits, we will also discuss the prominent case where the table is an actual trapezoid, studying the sets in parameter space relative to the three regimes. We prove in particular that the set for (1) has positive measure (giving a rigorous proof of the existence of Arnold tongues for internal-wave billiards), whereas the sets for (2) and (3) are non-empty but have measure zero. Joint work with C. Bonanno and G. Cristadoro.

In this talk, we are going to discuss a generalization to weighted blowups of the classical Castelnuovo' contraction theorem. Moreover, we will show as a corollary that the moduli stack of n-pointed stable curves of genus 1 is a weighted blowup. This is a joint work with Arena, Di Lorenzo, Inchiostro, Mathur, Obinna.

  In recent joint works with Civino, Gavioli and Scoppola, we studied the conjugacy classes of an elementary Abelian regular subgroup T of the symmetric group on 2ⁿ elements. In particular we computed, via GAP software package, a chain of normalizers in a Sylow 2-subgroup of this symmetric group defined iteratively, starting from T. We noticed that the logarithm of the indice of the (i-1)-th normalizer in the i-th normalizer of our chain is equal to the i-th partial sum of the sequence of the numbers of partitions of an integer in at least two distinct parts.
  In this talk we present some techniques developed in order to prove this result, including the notion of a special family of elements of a Sylow 2-subgroup, called rigid commutators. Finally, some generalizations to Lie algebras are given, considering similar results for an idealizer chain.

  In the early nineties Getzler discovered a nice algebraic structure on the equivariant homology of a topological conformal field theory. He called this algebraic structure a "gravity algebra" and he showed that it is governed by an operad which is closely related to the homology of M_0,n+1 , the moduli space of genus zero Riemann surfaces with n+1 marked points. A gravity algebra can be thought as a generalization of a (dg) Lie algebra, in the sense that other than the Lie bracket we also have higher arity operations which satisfies a "generalized Jacobi identity".
  In this talk we will first give an introduction to gravity algebras, providing many interesting examples from both algebra (cyclic cohomology of a Frobenius algebra) and topology (S¹-equivariant homology of the free loop space on a manifold). Then I will briefly explain that any class in the S¹-equivariant homology of the (unordered) configuration spaces of points in the plane H_*^S1(C_n(R);F_p) (with coefficients in a field F_p of p elements) gives rise to an homology operation for gravity algebras. After that we will see how to compute this equivariant homology and if time permits we will see some applications.

Let k be a finite field of chracteristic q. Let p,l be primes corpime to q and let N be a positive integer coprime to pql. In this talk we will define graphs X_l^q(Np^n) whose vertices are tuples (E,P,Q), where E/k is an elliptic curves and P,Q is a basis for E[Np^n]. The edges are given by degree l isogenies. We will discuss when X_l^q(Np^n)/X_l^q(Np^{n-1}) is Galois and will describe the structure of these graphs as volcanos. This is joint work with Antonio Lei.

Interpolation of differential forms is a challenging aspect of modern approximation theory. Not only does it shed new light on some classical concepts of interpolation theory, such as the Lagrange interpolation and the Lebesgue constant, but it also suggests that they can be extended to a very general framework. As an extent of that, it is worth pointing out that the majority of classical shape functions commonly used in finite element methods, such as those involved in Nedelec or Raviart-Thomas elements, can be seen as a specialisation of this theory. Of course, this generality brings along the evident downside of an unfriendly level of abstraction. The scope of this series of two seminars is thus twofold: presenting the main challenges of this branch of approximation theory but in a concrete manner. The first seminar will hinge on a development of a convenient one dimensional toy model that enlightens parallelisms and differences with usual nodal interpolation. In the second seminar will extend these techniques to the multi-dimensional framework, motivating our choices by a geometrical flavour. This talk is part of the activity of the MUR Excellence Department Project MatMod@TOV (CUP E83C23000330006).