HEGL Illustrating Mathematics Seminar

• Target audience: Bachelor students.
• Language of instruction: English.
• Supervised by: Florent Schaffhauser.
• Time and place: Monday 2:00-4:00 PM, in SR TBA (INF 205).

Introductory meeting: Monday 29.9, 2 PM, in SR TBA.

Logic, algebra and proof visualization

In this seminar, we explore how to represent mathematical objects, in particular proofs, using a programming language. We focus on basic results of logic and 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 a series of introductory videos that can serve as an introduction to the use of proof assistants. This will be produced collectively, using existing infrastructure, and no programmimg skills are required to participate in the seminar.

Constructive mathematics

Constructive algebra is algebra within the context of intuitionnistic logic.

It is often reduced, quite misleadingly, to mathematics without without the Axiom of Choice (AC), or even without the Law of Excluded Middle (LEM). But it should instead be thought of as a sum of algorithmic procedures for deriving proofs, which may or may not use AC or LEM.

Conceptually, this is made possible by an interpretation of mathematical statements in a way that lays the emphasis on computation. Existential statements, in particular, when interpreted in a constructive manner, call 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.

What we did last Winter

Ouputs of last year’s seminar:

• With Vincent Voß and Katrin Weiß. Algebra, Logik, und Beweisvisualisierung. Mitteilungen der Deutschen Mathematiker-Vereinigung, vol. 33, no. 3, 2025, pp. 205-209.
• Algebra, Logic, and Proof Visualization. Illustrating Mathematics: Reunion/Expansion, ICERM, 11-15.08.2025.

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.

Schedule for the talks

Date	Topic	Ref.
29.09	Introductory meeting
13.10
20.10
27.10
03.11
10.11
17.11
24.11
01.12
08.12	Status update meeting
05.01
12.01
19.01
26.01	Final presentations

References

Bridges, Douglas, and Fred Richman. 1987. Varieties of Constructive Mathematics. Vol. 97. Lond. Math. Soc. Lect. Note Ser. Cambridge University Press, Cambridge. London Mathematical Society, London.

Mines, Ray, Fred Richman, and Wim Ruitenburg. 1988. A Course in Constructive Algebra. Universitext. New York etc.: Springer-Verlag. https://doi.org/10.1007/978-1-4419-8640-5.