(Pro)Seminar on computer-assisted mathematics

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 tactics to prove algebraic identities.
• Understand logical reasoning and proof tactics.
• Formalize a piece of mathematics.