HEGL Illustrating Mathematics Seminar
Winter semester 2024-2025
- Target audience: Bachelor students.
- Language of instruction: English.
- Supervised by: Florent Schaffhauser.
- Time and place: Wednesday 2:00-4:00 PM, in SR 3 (INF 205).
- Zulip channel: (please register before October 25th, 2024).
Logic, algebra and proof visualization
In our digital age, computers provide new and original ways to visualize mathematical proofs. As the emphasis is placed on computability, we are encouraged to re-examine our daily mathematical practice and pay more attention to constructive methods.
In this seminar, we explore how to represent mathematical objects and proofs using computer programs. We focus on basic results of first-order logic and commutative algebra, which we prove without assuming previous knowledge in the field. Then we experiment with visualization tools for some of the proofs that we have encountered.
The expected output is an introductory tutorial program that can be run online. It will be designed collectively, using existing infrastructure, and no programmimg skills are required to participate in the seminar.
Constructive mathematics
The constructive approach to mathematics is often reduced (quite misleadingly) to mathematics without the law of excluded middle (LEM), or without the axiom of choice (AC). It should instead be thought of as a sum of algorithmic procedures for deriving proofs, which may or may not use LEM or AC.
Conceptually, this is made possible by an interpretation of mathematical statements in a way that lays the emphasis on computation. Existential statements, in particular, should be formally interpreted in a constructive manner (which calls for an explicit construction of an element satisfying a certain property).
Additionally, logic is not a pre-requisite in this approach. Instead, logical connectives and quantifiers are introduced formally in constructive mathematics, using the same language used to introduce mathematical objects.
References and schedule
The main reference for the seminar will be the book by Mines, Richman, and Ruitenburg (1988). Chapters 1 and 4 of Bridges and Richman (1987) are also recommended.
| Date | Topic | Ref. |
|---|---|---|
| 08.10 | Introductory meeting | |
| 16.10 | Sets and logic | Ch. I |
| 30.10 | Basic algebraic structures | Ch. II |
| 06.11 | Rings and modules | Ch. III |
| 13.11 | Divisibility in discrete domains | Ch. IV |
| 27.11 | Principal ideal domains | Ch. V |
| 18.12 | Status update meeting | |
| 15.01 | Design of final presentations | |
| 22.01 | Design of final presentations | |
| 29.01 | Design of final presentations | |
| 03.02 | Final presentations (HEGL Community Seminar) |
Design & Build
This webpage is produced using Quarto Markdown and VS Code. The slides are produced using Marp, also within VS Code. The website is published via GitHub Pages.