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, checked, and even discovered with the help of computers. The course combines foundational ideas from logic and proof theory with practical experience in formalizing mathematics.
Participants will:
- discover the theoretical foundations of proof verification,
- learn the syntax, tactics, and workflow of Lean,
- formalize mathematical definitions, statements, and proofs,
- work on an individual formalization project,
- present their work in an international research-oriented environment.
The course brings together advanced smaster students and PhD students from universities across Norway and abroad, creating a unique opportunity to engage with a growing international community at the interface of mathematics and computation.
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.