Just how bad of an idea is it for someone who knows programming and wants to learn math to try to work through a mathematics textbook with proof exercises, say Rudin’s Principles of Mathematical Analysis, by learning a formal proof system like Coq and using that to try to do the proof exercises?
I’m figuring, hey, no need to guess whether whatever I come up with is valid or not. Once I get it right, the proof assistant will confirm it’s good. However, I have no idea how much work it’ll be to get even much simpler proofs that what are expected of the textbook reader right, how much work it’ll be to formalize the textbook proofs even if you do know what you’re doing and whether there are areas of mathematics where you need an inordinate amount of extra work to get machine-checkable formal proofs going to begin with.
It’s a bad idea. Don’t do it. You’ll be turned off by all the low-level grudgery and it’ll distract you from the real content.
Most of the time, you’ll know if you found a solid proof or not. Those times you’re not sure, just post a question on math.stackexchange, they’re super-helpful.
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 stuff in it.
So is it possible that in the future we might be able to have something that’s to the present raw proof languages as Haskell is to basic lambda calculus, and that it might actually be feasible to write proofs on top of established theorem libraries with the highest level of proof code concise enough for comfortable human manipulation?
I also understand that Coq does some limited proof search based on the outline given by the human operator, which is another interesting usability groove on top of the raw language. Of course both using a complex, software-engineering like theorem library and giving proof-hints to a Coq style program are pretty obvious expert skills which you’ll expect to have after being quite familiar with knowing how mathematical proofs work in general.
I have tried exactly this with basic topology, and it took me bloody ages to get anywhere despite considerable experience with coq. It was a fun and interesting exercise in both the foundations of the topic I was studying and coq, but it was by no means the most efficient way to learn the subject matter.
The Metamath project was started by a person who also wanted to understand math by coding it: http://metamath.org/
Generally speaking, machine-checked proofs are ridiculously detailed. But it being able to create such detailed proofs did boost my mathematical understanding a lot. I found it worthwhile.
The way we teach proofs and mathematical sophistication is ad hoc and subject specific. I wish I knew a better general way, but barring that, perhaps start with a mathematical subject close to programming. For instance logic or complexity theory. I wouldn’t bother with proof assistants until you are pretty comfortable with proofs.
Just how bad of an idea is it for someone who knows programming and wants to learn math to try to work through a mathematics textbook with proof exercises, say Rudin’s Principles of Mathematical Analysis, by learning a formal proof system like Coq and using that to try to do the proof exercises?
I’m figuring, hey, no need to guess whether whatever I come up with is valid or not. Once I get it right, the proof assistant will confirm it’s good. However, I have no idea how much work it’ll be to get even much simpler proofs that what are expected of the textbook reader right, how much work it’ll be to formalize the textbook proofs even if you do know what you’re doing and whether there are areas of mathematics where you need an inordinate amount of extra work to get machine-checkable formal proofs going to begin with.
It’s a bad idea. Don’t do it. You’ll be turned off by all the low-level grudgery and it’ll distract you from the real content.
Most of the time, you’ll know if you found a solid proof or not. Those times you’re not sure, just post a question on math.stackexchange, they’re super-helpful.
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.
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 stuff in it.
So is it possible that in the future we might be able to have something that’s to the present raw proof languages as Haskell is to basic lambda calculus, and that it might actually be feasible to write proofs on top of established theorem libraries with the highest level of proof code concise enough for comfortable human manipulation?
I also understand that Coq does some limited proof search based on the outline given by the human operator, which is another interesting usability groove on top of the raw language. Of course both using a complex, software-engineering like theorem library and giving proof-hints to a Coq style program are pretty obvious expert skills which you’ll expect to have after being quite familiar with knowing how mathematical proofs work in general.
I have tried exactly this with basic topology, and it took me bloody ages to get anywhere despite considerable experience with coq. It was a fun and interesting exercise in both the foundations of the topic I was studying and coq, but it was by no means the most efficient way to learn the subject matter.
The Metamath project was started by a person who also wanted to understand math by coding it: http://metamath.org/
Generally speaking, machine-checked proofs are ridiculously detailed. But it being able to create such detailed proofs did boost my mathematical understanding a lot. I found it worthwhile.
“There is no royal road to geometry.”
The way we teach proofs and mathematical sophistication is ad hoc and subject specific. I wish I knew a better general way, but barring that, perhaps start with a mathematical subject close to programming. For instance logic or complexity theory. I wouldn’t bother with proof assistants until you are pretty comfortable with proofs.