Math Calendar
Seminar webpage https://webspace.science.uu.nl/~piero001/index_2025seminar_geometric_manin.html
Supervisor: Lola Thompson
Second reader: Marta Pieropan
Abstract: A positive integer n is a practical number if every positive integer upto and including n can be expressed as a sum of distinct divisorsof n. Schwab and Thompson generalized this notion by defining f-practicalnumbers: positive integers n for which every integer in a certaininterval can be expressed as a sum of f(d)-values for distinct divisors dof n, where f is an arithmetic function. One of theexamples they studied arises when considering f-practical numbers with f=s,where s denotes the sum-of-proper-divisors function. In this case,these integers are referred to as s-practical numbers.
In this talk, we discuss our research on the s-practical numbers. Wehave found various ways of establishing an upper bound on the count of s-practicalnumbers, of which we discuss two methods during this talk. Furthermore, wepresent a full classification of s-practical numbers with two primefactors, which contributes to a lower bound on the count of s-practicalnumbers.
Supervisor: Johan Commelin
Second supervisor: Wouter Swierstra
Abstract: Proof assistants like Lean enable the formalisation of mathematicalproofs in a machine-verifiable way, ensuring correctness to a higher degreethan proofs written in natural language. To achieve this, proof assistants arespecialized functional programming languages in which mathematicians must firstspecify how objects are encoded, before writing proofs about them.However, these encodings are more meticulous than the abstract reasoningtypical in mathematics, creating friction when proof assistants requiresubstantial effort for implementation details that mathematicians wouldconsider trivial.
In particular, a theoremshould remain valid when we change the encoding of the underlying objects toone more suitable for a given task. This transport of results across differentrepresentations, known as proof transfer, requires significant effort whenusing proof assistants. In this thesis, we examine Trocq, a framework designedto automate proof transfer, and present an implementation of it in Lean,discussing both implementation design choices and practical considerations forusers.
Title: The virial theorem and absence of eigenvalues of the N-Body Dirac Hamiltonian
Abstract:
The virial theorem is a powerful tool for proving the absence of eigenvalues of differential operators, granting that one can find an adequate auxiliary operator. In this presentation we discuss how this theorem has been used for the Klein-Gordon operator, and to what extent we could use a similar strategy for the existence of eigenvalues for the N-body Dirac operator, which is still an open problem. First, using a modified dilation operator we apply the theorem to a simplified model, consisting of a single-component first order operator with a bounded potential. Afterwards, we will analyse to what end we can just use the standard dilation operator instead, both for the simplified case and the N-body Dirac operator.
More info
More info
In this talk, we will see the Seiberg-Witten equations on cylinders and applications to the topology of four-manifolds. One application is the result that connected sums of four-manifolds with b⁺> 0 have vanishing Seiberg-Witten invariants, implying that symplectic four-manifolds are irreducible. Another application will be the minimal genus problem in four-dimensions: holomorphic curves in Kähler surfaces are genus minimizing in their homology class, and more generally, symplectic surfaces in symplectic four-manifolds are genus minimizing.
More info