Home Organisation Program Schedule Top

(Pro)Seminar on Computer-assisted mathematics

Picture of the Lean interface in VS Code

Judith Ludwig, Florent Schaffhauser
Heidelberg University
Summer Semester 2024

Organisation

The purpose of this (pro)seminar is give an introduction to computer-assisted mathematics, in particular the computer algebra system Sage and the interactive theorem prover Lean.

  • Target audience: Bachelor students.
  • Language of instruction: English.
  • Time and place: 4-6pm on Tuesdays, in Seminar Room 3 (INF 205).
  • Zulip channel:     (click on this link to register **before April 30th, 2024**).
  • GitHub repository:   CompAssistedMath2024  
  • Registration:   On Müsli.

This seminar is intended for beginners. More experienced students are welcome to participate as mentors/tutors.

Program

Topics of linear algebra to be covered in the seminar:

  • Computer algebra systems. Representations of vectors and matrices.
  • Row operations. Gaussian elimination. Row-reduced echelon form of a matrix.
  • Invertible matrices. Elementary matrices. Determinant.
  • Linear independence. Bases for the kernel and the image of a linear transformation.
  • Rank-nullity theorem and the row space of matrix. Basis for the row space.
  • Change of basis. Coordinates of a vector, matrix of a linear transformation.
  • Eigenvalues and the characteristic polynomial. Diagonalisation.
  • The Gram-Schmidt process. Least-square approximation.

Aspects of the Lean 4 programming language to be covered in the seminar:

  • Installation of a proof assistant. Familiarisation with the interface.
  • The Natural Number Game (Peano axioms and the induction principle).
  • Understand logical reasoning and proof tactics.
  • Understand tactics to prove algebraic identities.
  • Formalize a piece of mathematics.

Schedule

# Date Topic Speaker Slides Code
1 16/04 Introduction to Sage Instructors
2 23/04 Introduction to Git + Assignment #1 Instructors
3 30/04 Kernels, images and diagonalisation Working in pairs
4 07/05 Least squares approximation Working in pairs
5 14/05 Project prepararation Working in pairs
6 21/05 Project presentation
7 28/05 Introduction to Lean + Natural Number Game Instructors
8 04/06 Basic tactics + Assignment #2 Instructors
9 18/06 Advanced tactics Instructors
10 02/07 Project preparation Working in pairs
11 16/07 Project presentation 1
12 23/07 Project presentation 2