ForAlli weekly meetings
In the Spring semester 2023, the Formalization Alliance will continue weekly meetings on Thursdays at 4pm in U523 (Top Lounge).
Everyone is welcome!
ForAlli Zulip chat
Our communication channel is the Zulip chat:
https://foralli.zulip.cs.aalto.fi
You can log in with your Aalto account. Welcome!
Mathematical proofs
Universal truths are what mathematics is about. Precise statements which have been established as true are called theorems. And how the truth of a theorem is established is by giving a logically correct proof, deriving the stated conclusion from the stated assumptions, i.e., the hypotheses.
Well, you may ask: what does it mean that a theorem statement is phrased precisely? And what qualifies as a logically correct proof?
You are seeking deeper understanding of mathematics itself. Welcome!
Formalized proofs
Humans make mistakes (correct me if I'm wrong). For universal truths, we can't afford mistakes! Could a computer verify each step of the logical reasoning in our mathematical proofs?
Absolutely! Feed into your laptop both the statement and its proof in a language that the machine can understand, and the computer will be happy to tell you what it thinks of it.
You also get to explore mathematical knowledge via programming. Like the idea? Welcome!
The foralli blog
Blog Posts
-
First steps
created by
Mar 03, 2022
-
Launching the Formalization Alliance
created by
Dec 17, 2021
