What use are theorems?

Stream: general

[Andre]

Hi everyone.

I'm trying to wrap my head around theorems. Are they used for things like optimizations? For example, I understand that when you want to compress a file like a video you do so because you want to keep as much visually useful information whilst also keeping down on size for transferring. So my question is if compression tools are just Theorem algorithms. Some are more efficient than others or achieve different goals. Or is the theorem like a small subset of the algorithm?

Thanks!

[Riccardo Brasca]

I have the impression your question is not clear. In mathlib we use the word "theorem" to mean a mathematical theorem. Are you asking how we can write similar stuff using a programming language?

[Andre]

So I understand that the programming language is used to check itself. Self-validate the proofs. However, it can still be used to create things. That blows my mind and I want to understand it. Maybe I need to try and play with it more to understand.

[Johan Commelin]

@Andre The theorems don't create anything. They only "validate" as you say.

[Kyle Miller]

Theorems don't have much to do with compression. They're mathematical truths, and you can use them to guarantee that certain conditions you might depend on are met. For example, if you imagine all the natural numbers (0, 1, 2, 3, and so on) stretched out in front of you, and you start crossing off every other number starting from 0, the following is a theorem: you will eventually cross off every even number, and you will only cross off even numbers. This is a theorem explaining what this simple crossing-numbers-off algorithm does.

In Lean, a theorem is like a program that processes and creates truths, and you can write proofs of theorems using the exact same functional programming language you use to write more traditional algorithms/programs (though usually we use tactics to construct proofs). Have you done the Natural Number Game yet? It's all about proving theorems about natural numbers in Lean.

[Johan Commelin]

You need definitions to create something.

[Andre]

Thank you I have played but not completed yet. Thank you for the guidance.