Project Computer Assisted Proofs

Doel vak

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.

Inhoud vak

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)

Aanvullende informatie onderwijsvormen

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.

Toetsvorm

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%.

Literatuur

To be made availabe online on Canvas

Aanvullende informatie doelgroep

Bachelor Mathematics, year 3

Overige informatie

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.

Aanbevolen voorkennis

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.