Project Computer Assisted Proofs

URL study guide

https://studiegids.vu.nl/en/courses/2025-2026/XB_0039

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 rigorousness/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 fulfill.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)

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 4
- 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 available online on Canvas

Target Audience

Bachelor Mathematics, year 3

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.