Written by Mirka Langenhorst
3Blue1Brown, Alexander Thomas, simpleclub, Mathepeter and MathemaTrick: many students of our generation use videos to get a grasp of complicated topics. As a goal of the “Illustrating Mathematics“ Seminar we tried to do that for another (complicated) theorem: The Fundamental Theorem of Algebra (FTA).
To add a twist to the FTA, we made a video about the Discrete Fundamental Theorem of Algebra, proved constructively. What this is all about, you will read in this blog post, describing our journey on the topic of Logic, Algebra and Proof Visualization, which led us to see mathematics in a new light.
In this HEGL seminar, a group of six students, Alejandro Intriago, Cara Kahlau, Jonas Heese, Kateryna Driuk, Mirka Langenhorst and Nele Bundfuss, first learned about the theoretical part of constructive algebra by giving talks based on different chapters of the book A Course in Constructive Algebra by Mines, Richman and Ruitenburg (1988). Then, we decided to look further into the proof of said Discrete Fundamental Theoreom of Algebra in order to create a visualisation as well as creating a new level for the „Lean Game“, which was set up by the group of last years Illustrating Mathematics seminar (take a look at https://doi.org/10.1515/dmvm-2025-0058). In this process, we tried to make constructive mathematics accessible and fun to our audience of hopefully many interested mathematics students (and potentially all their friends and family, too!).
To get there, we had to ask ourselves first: What does constructive mean?
Logic, Algebra and Proof Visualization
In classical algebra, we often use certain logical principles implicitly. One of the most fundamental ones is the idea that if the non-existence of a mathematical object (here: \(x\)) leads to a contradiction, then the object must exist:
\((\neg \exists x \Rightarrow \bot) \Rightarrow \exists x\).
More generally, classical mathematics assumes that every mathematical statement is either true or false (this is also called the law of the excluded middle), even if we have no way of deciding which is the case.
\(\,p \vee \neg p\).
This style of reasoning often leads to existence results that guarantee that an object exsists, but don’t say anything about how to find it.
That’s where constructive mathematics comes in. Rather than focusing on which logical principles are allowed or forbidden, the attention shifts to the meaning of mathematical statements. In this different interpretation, a proof isn’t just a logical argument, but the procedure of constructing a solution or at least constructing the tools along the way.
Circling back to our initial example, this means that an existential statement is only considered meaningful if it comes with a method that tells us exactly how to construct the object which satisfies the required property.
Speaking metaphorically, one could say that classical mathematics can tell you all the important places in a city. Intuitively through seeing pictures or hearing stories, we know or trust that the Eiffel Tower or the Brandenburg Gate exist, because we weren’t given any reason to mistrust the information. But constructive mathematics requires you to be able to describe how to get there to convince yourself of their existence.
Having that in mind, a new perspective to mathematics had openend up to us. Working without familiar intuitive shortcuts was challenging at first, but it also changed how we saw proofs and defintions. Throughout the seminar talks, we gradually got more comfortable with the construction of mathematical proofs and the constructive approach of it all.
Proving the Discrete Fundamental Theorem of Algebra
Before we start, we first have to recall what the Fundamental Theorem of Algebra states and get an overview of the terms used, so that we can move on to more advanced concepts.
The simplest definition of the FTA states that every nonconstant polynomial \(P(X)\) has at least one complex root.
Equivalently, one can say that the field of complex numbers is algebraically closed.
Why is our FTA called “discrete”?
That is, because we’re looking at the classical FTA applied to the rational numbers \(\mathbb{Q}\), which is a discrete field, as well as its algebraic closure. Here, discrete describes the property of being able to tell if two elements are apart.
And why is it called “constructive”?
Our proof is constructive as the objects we use are, in fact, constructable and follow the guidelines as mentioned in the previous paragraph on “Logic, Algebra and Proof Visualization”.
To get some intuition on the topic, we’ll walk you through the simplified proof of the DFTA:
In order to prove that any polynomial in \(\mathbb{Q}\) has at least one root in \(\mathbb{Q}\) we can use the property of \(\mathbb{Q}\) being algebraically closed, as this is equivalent to the former.
Assume we already know that the field of the complex numbers \(\mathbb{C}\) is algebraically closed. Let \(P(X)\) be a polynomial whose coefficients are algebraic numbers. Since each coefficient is algebraic over the rational numbers \(\mathbb{Q}\), there exists a finite field extenstion \(L/\mathbb{Q}\) that contains all of them. Now, because \(\mathbb{C}\) is algebraically closed, the polynomial \(P\) has a root \(\beta \in \mathbb{C}\). Consider the field \(L(\beta)\) obtained by adjoining this root to \(L\). Since \(\beta\) satisfies a polynomial equation over \(L\), the extension \(L(\beta)/L\) is finite. But \(L/\mathbb{Q}\) was already finite, and a finite extension of a finite extension is again finite. Hence \(L(\beta)/\mathbb{Q}\) is finite, which means that \(\beta\) is algebraic over \(\mathbb{Q}\). In other words, every root of \(P\) is an algebraic number, and so the field of algebraic numbers is algebraically closed.
All the work in this argument is hidden in one decisive step: the existence of a root \(\beta \in \mathbb{C}\). This existence ultimately relies on the fact that \(\mathbb{C}\) itself is algebraically closed – which is a highly nontrivial theorem.
But what if we do not assume this? What if we try to build the argument without relying on that powerful existence statement?
This is precisely where the constructive perspective becomes interesting – and where our video comes in.
The creation of the video
The process of the video making started of with creative brainstorming: Here, we sat together in the HEGL and decided on the framework and the style of the video. We discussed if the video would be of one of the team explaining and the visualizations popping up around him or if it should be explanatory text accompanied by a voiceover. We decided on the latter to set a focus on the proof and it appeared to be easier to follow along. On top of that, Alejandro came up with a funny introduction and outroduction.
Afterwards we took a closer look at the proof. To create an easily accessible video, we had to understand the DFTA in its essence first. This was followed by creating a script for the video: Nele wrote down a detailed script on what we wanted to present in the video, where we would simplify the subject and how we would insert the examples.
At the same time, Alejandro began to film the introduction, and as soon as the script was ready, the explanations followed.
As soon as they had material to work with, Cara and and Kateryna began to edit the video. Cara came up with the colorful design and the chalkboard background. We used the program Canva, which made it easier to integrate fun templates and edit the video.
In a January meeting, we finally filmed the outro; after that, Cara and Kateryna finalized our video, which you can now watch here:
Development of the Lean Game Level
Credit for this goes out to Jonas, who created the new Lean Game level. He describes the process as follows:
First of, we needed to come up with what theorems and results we wanted to formalize to begin with. We decided on two topics: The first being the decidability of the equality relation in
\(\mathbb{N}\), based on the first talk. The second being establishing elementary results about general strict inequalities on general ‘sets’/types.
After we decided on what to do, we started with the formalization process. This in turn proceeded in two phases, first we needed understand what the statements and objects meant precisely, and then formalize the definitions of the objects and theorem statements. In the second phase, we formalized the theorem proofs and created auxiliary lemmas for those as necessary.
In the third step, we compiled the template game from GitHub and started implementing the levels. Here, we needed to decide precisely which tactics – algorithms in the Lean Engine which solve (simple) theorem propositions – could be used to prove the theorem statements given. In this, we needed to be careful to not include tactics which were either too strong, one-shotting the theorem proofs, nor include nonconstructive axioms in the proofs.
After working this out, we are now able to present you this new level of the Lean Game. Have fun!