| Note | ||
|---|---|---|
| ||
On Wednesday 1618.10. at 16:15 there will be a Finnish Mathematical Society online colloquium talk on formalized mathematics, given by professor Heather Macbeth (Fordham University). Details about the talk can be found in the departmental seminar list. |
| Info | ||
|---|---|---|
| ||
For the time being, there are no planned regular meetings of ForAlli. |
| Info | ||
|---|---|---|
| ||
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 | ||
|---|---|---|
|
