3 ms·
mathematicians writing for peers don’t aim for the maximally explicit proof. details are frequently left out as obvious to the knowledgeable reader. leaving out
by aoki 8y ago
mathematicians writing for peers don’t aim for the maximally explicit proof. details are frequently left out as obvious to the knowledgeable reader. leaving out tedious matter is a matter of professional style, like tightening regular prose so it doesn’t club the reader over the head with every detail. (my instructor in Fourier analysis would subtly grimace at my very explicit proofs in office hours, but he knew i was a computer scientist so he politely said nothing because he knew it would do no good ;-)
- throwaway080383 8y agoI would also add that by and large this isn't done because of ego, but simply brevity. Seminal papers are often already hundreds of pages long, so to add every detail would bloat them to thousands of pages. And in any case, "skipping steps" is exactly how the top mathematicians think about the proofs when creating them.
- loup-vaillant 8y agoYeah, well, paper sucks. http://worrydream.com/#!/ScientificCommunicationAsSequentialArt http://worrydream.com/#!/ScientificCommunicationAsSequential... No mathematician today doesn't have access to a computer. Just fold the proof to some appropriate coarse level by default, and let the reader expand any part they want to read. It's not like our computers had any meaningful limit on how big a mathematical proof could be.
- AnimalMuppet 8y agoI think the limit may be the author, not the tool the author writes with.
- loup-vaillant 8y agoHistorically, there was always a limit to how big a paper could be to make it into a journal. Papers that aren't meant to make it into a journal are often way bigger.
- MAXPOOL 8y agoCurrently explicit formally verifiable proofs provide no value for most mathematicians apart from some specific fields. This may gradually change if proof assistants and proof checkers improve. It may become to incorporate some machine learning aspects and let algorithms search proof space that is too tedious for humans. This would finally turn computer into bicycle for mathematician.
- westoncb 8y agoAfter graduating with a CS degree and a repetitive strain injury, I decided to teach myself mathematics properly (so I could do technical/creative things without a computer). I took the project very seriously, working part-time at a grocery store with no other obligations on my time than learning. I would say the two biggest difficulties were 1) Undoing all the very bad math education I'd received earlier in life, and associated repulsion that came from it 2) Figuring out that when I ran into walls understanding certain things it could always be reduced to gaps in my knowledge that were implicitly assumed to not be there. I often ran into that reading proofs in the early days and wanted nothing more than 'very explicit' proofs as you describe (I used to always write mine that way too! In part because it's what I wished the authors were doing). I'd like to build something in software that automatically associates expandable annotations to mathematical notation, e.g.: http://images.slideplayer.com/34/10244075/slides/slide_5.jpg http://images.slideplayer.com/34/10244075/slides/slide_5.jpg —It would be super annoying if all the text were always revealed, but with a little cleverness and imagination I think a good scheme could be developed which would satisfy both beginners and experts. I would want a standard library of annotations which would automatically get associated just by using certain standard notational elements. Here's another demo I put together to try out the same concept for natural language documents: http://symbolflux.com/lodessay/ http://symbolflux.com/lodessay/