The pilot version of the course “Computer-assisted Mathematics” runs at UiT in the 2026 Fall term.
Computers are transforming modern mathematics. From testing conjectures to verifying deep theorems, computer-assisted reasoning is becoming an essential tool across pure and applied mathematics. This course offers a hands-on introduction to one of the most exciting developments in contemporary mathematics: formal proof verification.
Using the interactive theorem prover Lean and its rapidly growing mathematical library Mathlib, students will explore how mathematical proofs can be written and checked with the help of computers. The course combines foundational ideas from logic and proof theory with practical experience in formalizing mathematics.
Designed primarily for students in pure mathematics, the course is especially suitable for those curious about the future of mathematical research, theorem proving, and the role of formal methods in science and technology. Students should already be comfortable writing mathematical proofs and eager to explore cutting-edge tools that are reshaping the discipline.
The course is worth 5 credits (pass/fail). It follows a compact course format consisting of six interactive lectures over two weeks followed by two weeks of project work. Instead of an exam there will be a formalization project which can be completed collaboratively in small groups. All lectures will be live-streamed via Teams and recorded.
The schedule is:
The development of this course was funded by EUGLOH. We also greatfully acknowledge funding by CIMPA which allows selected external students to visit Tromsø for the duration of the course and for others to participate online.