Bachelor in Mathematics Student Task 2022

We group students from the six universities of the 4EU+ alliance to work on joint projects!

Each group of students is composed of one student per university. Each group of students has one mentor. Each mentor is responsible for his/her own students and for his group. Don't hesitate to contact the coordinator or the various contact persons below for more information! For Copenhagen students, this can take the form of a PUK project.

Starting date: February 7, 2022 (blok 3 for Copenhagen).
Final week: between April 4 and April 18, depending on time constraints

  • Copenhagen - Interactive theorem proving in Lean
  • Heidelberg - Efficient algorithms and graphs
  • Milan - Modular arithmetic and public-key cryptography
  • Paris - Arithmetic of series
  • Prague - Geometric inequalities
  • Warsaw - Optimal stoping theory

Copenhagen

Mentor: Lars Kühne
Contact person: Lars Kühne and Fabien Pazuki
Topic: Interactive theorem proving in Lean

Description:
Motivation: Computers played an essential role in the proof of various important theorems like the four-colour theorem (1976) and the Kepler conjecture (1998). However, their use was restricted to those parts of the proofs that only required a lengthy mechanical case analysis.

Nowadays, interactive theorem provers allow the verication of virtually any mathematical theorem in a collaborative effort between machine and human; the most prominent such proof assistants are Coq, Isabelle, and Lean. In practice, few theorems at the level of present research have been formally checked by these tools, but the practical possibility has been demonstrated in some cases, for example with the formal verification of the Kepler conjecture in 2017 and the very recent success within the liquid tensor experiment proposed by Scholze.

Unfortunately, the translation of a proof in a mathematical article or textbook to one that is veriable by a proof assistant can still be a very tedious task. In their argumentation, mathematicians often rely on intuition and a knowledge of many fundamental results. In recent years, the Lean community has built a mathematical library containing basic proof tactics and verifed proofs, which should eventually cover at least the complete curriculum of an undergraduate student in mathematics.

Project Description:
In this project, we study the Lean Theorem Prover that came out in its first version in 2013 (written by Leonardo de Moura, Microsoft Research) and in its most recent fourth version in 2021 (for practical reasons, we will use Lean 3 instead of the most recent version Lean 4).

In recent years, a substantial mathematical library (i.e., a collection of formalized definitions and proofs in Lean) has been built by the Lean community. Our aim will be to get a first working knowledge of both.

The project falls in three phases (this is a preliminary plan, there may be changes!):

  1. exploring the Lean programming language (approx. 3 weeks): a pragmatic
    introduction to the basic features of Lean (formal proof verification, dependent
    type theory, calculus of constructions)
  2. exploring undergraduate mathematics in Lean (approx. 3 weeks): a look
    at some actual ``undergraduate" mathematics done in Lean; tutorials with ``real
    mathematics"; identification of topics for own projects
  3. own projects (approx. 6 weeks): work on specific problems; in-person meeting
    in Copenhagen

Time Frame:
10-12 weeks in total, submission deadlines after agreement between the participants and the coordinator.

Prerequisites:
The students

  1. have a mastery of first-year undergraduate mathematics,
  2. appreciate rigorous formal mathematical arguments and proofs, such as those that one should encounter in first-year lectures, e.g. epsilon-delta-arguments,
  3. are able to set up a working environment for Lean 3 on their computer, following instructions,
  4. (optimally, not mandatory) have already some basic exposure to Lean (e.g., by trying to play the natural number game of Buzzard),
  5. (optimally, not mandatory) have programming experience, even better if in a functional programming language (e.g., Haskell).

Note that the learning curve during the project may be steep so that enduring motivation is required.

Learning Outcomes:
The students will then be able to

  1. use dependent type theory as a foundation of mathematics (instead of set theory),
  2. read and write correct, maintainable Lean code,
  3. translate mathematical theorems (in the context of an undergraduate curriculum) to Lean definitions and theorem statements,
  4. use basic strategies to verify such theorems in Lean by translating and adapting proofs from textbooks,
  5. search and find results in the mathematical library of Lean (mathlib),
  6. communicating problems (e.g., missing or unsuitable basic results), goals, and ideas to other members of the Lean community.

Workload:
In the first (and most of the second) phase, we will meet regularly over Zoom, twice a week, for a total of about 180 minutes per week. In later phases, we meet as needed. It is expected that you do tutorial exercises (some in the form of two
assignments) as well as acquire some information from Theorem Proving in Lean on your own in addition to our meetings. For the third stage of the project, you should be prepared to code about 5-8 hours a week.

Evaluation:
(preliminary information, to be confirmed:) Students receive a Danish grade (12, 10, 7, 4, 02, 00, -3). You will receive a grade "a" for the assignments (tutorial exercises) and a grade "b" for the work on your own project (code + written report + oral presentation). The final grade is then `a/3+2b/3’, rounded to the next grade (up in case of equidistance).

If you receive a numerical grade for this project with your local university, some conversion schemes will be applied. If you only receive a pass/fail, then all grades except 00 and -3 mean a pass.

Heidelberg

Mentor: Michael Winckler
Contact person: Michael Winckler and Theresa Möcke
Topic: Efficient algorithms and graphs
Lecturer: Dr. Michael Winckler (Heidelberg University), Dr. Susanne Krömker (Heidelberg University)

Description:
Graphs are a central model in discrete mathematics. They are used to derive representations of weighted networks and to solve application problems on these networks using algorithms for efficiently dealing with data and structure of the underlying graph.

In this student task we will investigate classical graph problems along with the state-of-the-art methods to derive solutions to these models. We will analyze the complexity of the used algorithms and the effect of complexity classes on the runtime behaviour of such algorithms in practise.

The student task aims to both understand the theoretical concepts and implementation issues for the practical use in computer code. While it is helpful for some task topics to have a background in computer programming and implementation, participation is also possible for students with purely a mathematical background.

Target group:
Students from year 2 and 3 (bachelor mathematics)

Prerequisites:
“Analysis I”, “Linear Algebra I”
(“Introduction to Programming” is a plus, but not necessary)
(“Introduction to LaTeX” is a plus, but can be learned alongside)

Learning Goals:

  • Participants will know and understand the principals behind several classical algorithms on graphs (Dijkstra’s Algorithm, Perfect Matching, A*, Minimal Spanning Trees …).
  • Participants will be able to compute the complexity of algorithms and understand the difference between various complexity classes.
  • Participants will document the theory and background of one of these algorithms both in written documentation and on a wiki page.

Literature:
D. Jungnickel “Graphs, Networks & Algorithms” Springer Heidelberg, ISBN 978-3-642-32278-5

Milan

Mentor: Ottavio Rizzo
Contact person: Ottavio Rizzo
Topic: Cryptography
Title: Modular arithmetic and public key cryptography

Description:
We will study applications to cryptography of arithmetic properties of congruences.

Modular arithmetic is the main ingredient for public key cryptography, the technique that allows people to have a private conversation in a public space without the need to share in advance a secret key. In the 2021 BMST project we studied in particular the issue of computing a multiplicative inverse in modular arithmetic and Pollard’s Rho Algorithm for factorization (one of the earliest modern factorization algorithms). In the 2022 BMST project we will once again begin with discovering what is public key cryptography and how modular arithmetic plays its role in the game, to later focus on how to efficiently compute the greatest common divisor of two integers and how to (inefficiently) solve the discrete logarithm problem.

Prerequisite is the first year of algebra (groups, rings, fields, modular arithmetic); some programming experience and familiarity with LaTeX is good but not strictly necessary.

Paris

Mentor: Pierre Charollois
Contact person: Pierre Charollois
Topic: Arithmetic of series

Description:
It is a famous result going back to Euler that the value of series 1+1/4+1/9+1/16+... equals Pi^2/6. We will consider higher dimensional analogs of this series, a typical example being the summation of 1/(n+m)^2(5m+3n)^2, where n,m runs over integers, or more generally 1/(a.n+b.m)^2(c.m+d.n)^2 for fixed integers a,b,c,d.

The value of these sums is effectively computable, and depends in a subtle way on a,b,c,d. The aim of the project is to obtain an algorithm to compute easily with these sums, to the point of being able to experiment/establish some of their finer arithmetic properties.

The code, some of its outcome and the theoretical results will be presented in the written report.

The tools will involve a wide range of topics from analysis and effective algebra, including Fourier series, Lattice reduction and the Euclidean algorithm to p-adic integers.

Time Frame:
10-12 weeks in total, submission deadlines after agreement between the participants and the coordinator.

Prerequisite is the first year of algebra (groups, rings, fields, modular arithmetic); some programming experience and familiarity with LaTeX is good but not strictly necessary.

Prague

Mentor: Pawlas Zbynek
Contact person: Pawlas Zbynek
Topic: Geometric inequalities

Description:
By a geometric inequality we mean any inequality involving various measures of geometric objects. The geometric inequalities could deal with size measures (lengths, areas, volumes, etc.) as well as measures connected with shape (angles, number of vertices, etc.). Everyone knows the triangle inequality, probably the most important and oldest geometric inequality. In the first year of BMST project, we focused on the isoperimetric inequality. In the planar case it states the inequality between area and perimeter. It implies that for a given perimeter, the circle has the largest area. A related question is what figure of a given diameter has the largest area (isodiametric problem). Another related problem is what figure of a given constant width has the smallest area (Blaschke-Lebesgue theorem).

The aim for BMST 2022 is to study various geometric inequalities. In addition to the isodiametric inequality and the Blaschke-Lebesgue theorem, we can also consider other types of inequalities (different trigonometric inequalities, Brunn-Minkowski inequality, etc.). At the beginning each student (or smaller group of students) will be assigned one inequality to investigate. The students will elaborate the proofs and work out some examples. The results will be summarized in the report and presented on the wiki page of the project.

Warsaw

Mentor: Witold Bednorz
Contact person: Witold Bednorz
Topics: Optimal stoping theory

Description:
The theory of probability began with efforts to calculate the odds in games of chance. In this context optimal stopping problems concern the effect on a gambler's fortune of various possible systems for deciding when to stop playing a sequence of games. The standard application is statistical inference, where the experimenter must constantly ask whether the increase in information contained in further data will outweigh the cost of collecting it.

Optimal stopping theory provides a general mathematical framework in which such problems can be precisely formulated and in
some cases solved completely. In this introduction we shall present four simple examples which illustrate some of the problems that arise in the general theory.

The outline for this project is as follows:
1) Introduction to optimal stopping
2) Doob's optional sampling theorem
3) Finite horizon - snell envelop
4) Selected applications: e.g. secretary problem
5) Selected applications: e.g. rational thief problem
6) Selected applications: e.g. discrete Black-Scholes model
7) Infinite horizon - assumptions - monotonic case
8) Randomized stopping rules

Requirements:
Basics of probability theory - random variables, independence.

Goals:
To understand basics of optimal stopping theory, compute Snell's envelope in some cases, know main examples for the theory.

Contacts

  • Charles University (Prague)
    Zbynek Pawlas (email: pawlas"at" karlin.mff.cuni.cz)
  • Heidelberg University
    Michael J Winckler (email: Michael.Winckler "at" iwr.uni-heidelberg.de) 
  • Sorbonne University
    Pierre Charollois (email: pierre.charollois "at" imj-prg.fr)
  • University of Copenhagen
    Lars Kühne (email: lk "at" math.ku.dk)
  • University of Milan
    Ottavio Rizzo (email: ottavio.rizzo "at" unimi.it)
  • University of Warsaw
    Witold Bednorz (email: wbednorz "at" mimuw.edu.pl) 

Coordination: Fabien Pazuki (email: fpazuki "at" math.ku.dk)