Mathematicians have come up with formal languages that can, in principle, be used to write proofs in a way that they can be checked by a simple algorithm. However, they're utterly impractical. Most proofs leave some amount of detail to the reader. A proof might skip straightforward algebraic manipulations. It might state an implication and leave the reader to figure out just what happened. Actually writing out all the details (in English) would at least double the length of most proofs. Put in a formal language, and you're looking at an order-of-magnitude increase in length.
That's a lot of painstaking labor for even a simple proof. If the problem is the least bit interesting, you'll spend a lot more time writing out the details for a computer than you did solving it.
Mathematicians have come up with formal languages that can, in principle, be used to write proofs in a way that they can be checked by a simple algorithm. However, they're utterly impractical.
I understood that a part of the univalent foundations project is to develop a base formalism for mathematics that's amenable to similar layered abstraction with formal proofs as you can do with programs in modern software engineering. The basic formal language for proofs is like raw lambda calculus, you can see it works in theory but it'd be crazy to write actual s...
This thread is for asking any questions that might seem obvious, tangential, silly or what-have-you. Don't be shy, everyone has holes in their knowledge, though the fewer and the smaller we can make them, the better.
Please be respectful of other people's admitting ignorance and don't mock them for it, as they're doing a noble thing.
To any future monthly posters of SQ threads, please remember to add the "stupid_questions" tag.