Project Computer Assisted Proofs

Course Objective

At the end of this course students will be able to ...

... explain the different roles, possibilities, and limitations that
computers currently bring for obtaining mathematical proofs.
... give an informed opinion (concerning issues like
rigourousness/completeness, necessity) of such computer uses in several
different situations.
... describe several different techniques and software tools available
for computer assisted proofs and the different purposes they fulfil.
... apply at least one such tool and corresponding techniques in a
detailed technical case study.
... work together in a small group on a project about computer assisted
proofs.
... present part of the project in both written and oral form.

Course Content

This course introduces several different roles that computers can play
in assisting mathematicians to obtain rigorous proofs for various
mathematical statements. The relevant mathematical areas are manifold.
They range from pure to applied, and include fields such as dynamical
systems, number theory, graph theory, optimization, geometry, and
cryptography. Examples include the proofs of the  4-colour theorem, the
Kepler conjecture, the existence of a Lorenz attractor, etc.

Some topics (with partial overlap)
- Representing mathematics in computers and performing computations
(data structures, algorithms)
- Reducing a mathematical problem to one solvable (in principle) by a
computer, efficiency issues
- Proof certificates, finding vs checking them
- Interval arithmetic, rigorous numerics
- Formal theorem proving (using Lean)

Additional Information Teaching Methods

The first week is a mix of lectures and tutorial (computer) sessions,
introducing the students to various theoretical and practical aspects of
computer assisted proofs. At the end of this week, the students choose a
project on which they work in groups of about 3 - 5 students for three
weeks. Each group meets about 2 or 3 times per week with a teacher. In
the final week, each project group is responsible for giving an oral
presentation and handing in a written report about the project work.

Method of Assessment

In the first week, students have to hand in several assignments, which
all have to be marked "pass" in order to pass the course. The oral
presentation counts for 30% towards the final grade and the written
report counts for 70%.

Literature

To be made availabe online on Canvas

Additional Information Target Audience

Bachelor Mathematics, year 3

Additional Information

This course is still in development. Deviations from what is written in
the study guide may be announced at the start of the course via Canvas.

Recommended background knowledge

Familiarity with programming (e.g. Python from X_400629) and software
for computer algebra/scientific computing (e.g. Mathematica from XB_0006
and Matlab from X_401039). Basic mathematical background (as covered by
the first two years of the bachelor programme) in linear algebra,
discrete mathematics, and analysis.