81–90 of 107 posts
Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project. [1] https://en.wikipedia.org/wiki/Coq [2] https://github.com/UniMath/UniMath
Earlier quoted context omitted.
Also, that is quite a remarkable and provocative statement given that Andrew Wiles is still very much alive.
Sure, Wiles obviously understands the main thrust of his proof. But one could argue that Wiles' result depends on lots of other results, which in turn depend on other results, and so on through decades and decades of work, ultimately going back to the foundations of mathematics. Neither Wiles nor anybody else can claim to rigorously understand all of it. You can imagine this as a tree, with Wiles' work as root, and h…
And finally from the beginning of math people misunderstand their on theorems, doesn t mean that there students won t do better.
Headline is waaaay overblown, but not all of it is total hyperbole -- checkout out arxiv and try to read the abstract from just about any paper. It's basically totally impermeable. I'm almost done with an undergraduate degree in math and basically have no idea what ~90% of the research is about at anything other than a topical level. This is fine, it's written for specialists in the field (hopefully), but damn, for m…
I did some undergraduate research and ended up getting published. My initial drafts were written with prose so that I (and hopefully any novice) could understand. However, my professor wasn’t happy with it so I got some help from one of his grad students to re-write it. By the end of it I could barely understand my own paper. IMO the final paper had too much technical jargon which was convoluting some simple concepts…
This is symptomatic of IMHO the biggest single problem with the world of mathematics today. This discipline should be about developing ideas based on rigorous foundations and logic, which is a useful and important purpose. Once you have understood those ideas, even "advanced" results often seem quite simple and intuitive, and we can take that understanding and apply it to other work if helps us to make useful progress. However, the amount of needlessly obscure terminology, poor notation and just plain bad writing in formal papers make the whole field absurdly inaccessible, even to many who might have no trouble understanding the underlying concepts and important results.
Just imagine what would happen if we tried to write engineering specs or software the way postgraduate mathematics research is done. We'd be trying to debug source code where every identifier was a single character, taken from one of three or four different alphabets, with several of them looking similar enough to mistake one for another, with a bunch of combining accent modifiers on top that were used to fundamentally change the semantics of the program, interspersed with comments by someone who needs a remedial class in basic writing skills, full of technical terminology that is defined in terms of other technical terminology from other software packages, except that sometimes the meaning is subtly different in this context but that isn't noted anywhere on the screen at the time, resulting in needing to spend half an hour doing a depth-first-search of all the definitions only to find that a function whose only identifier is the name of the developer who wrote the second version (because the first person to work on it already has another function bearing their name) is actually equivalent to what a programmer would write as
const DAYS_IN_WEEK := 7
I'm currently working on the formalization of Catalan's conjecture (or Mihăilescu's theorem) in Isabelle/HOL/Isar. My personal impression is that more formal verification is necessary in math, and it should be tought to every student of Mathematics in introductionary courses because it gives an unforgiving but also rewarding learning experience with formal proofs. Feel free to ask questions.
On the other hand, we do need to build a standard library of results that can be used to prove those newer results. You can't do much in analysis without basic results on metric spaces, for instance.
Earlier quoted context omitted.
So I find this interesting, because it seems to confirm a suspicion I held. I "only" did some undergrad math during my computer science (but due to a lack of specialization at my university back then it was "real math", i.e. we took the same courses as the math students). My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it…
> My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it sound harder than it really is. I never dared to postulate that this is a more general problem of math, but your words sound like that's exactly what is happening. I "only" have a masters degree in Math, but this sounds really wrong to me. Most advanced math concepts are…
Certainly some advanced math concepts require a lot of foundations and therefore take time to build up to them, but usually the individual steps along the way should be quite accessible if well presented.
To follow up on one of your own examples, suppose we have someone who understands the basic ideas of abstract algebra, say someone who had done a first course in topics like groups and rings as part of their undergraduate studies. (I note in passing that even a keen school student considering studying maths at university might be able pick up these concepts with good presentation in a few days.) Then suppose that person are curious about why there is a quadratic formula but people claim that not only do we not know of any corresponding quintic formula, in fact we can prove that no such formula is possible.
Explaining the concepts and key results from Galois theory needed to get to that proof shouldn't take months. There are lots of technical terms like solvability by radicals and field extensions and quotient rings and so on, but if these concepts are properly explained, none of them would in itself be more than a typical undergrad student could understand after a few minutes. Building up the argument would of course take longer than understanding any given step, but it's not prohibitively difficult or complicated.
Unfortunately, in many university lectures and textbooks, those concepts are introduced using only a mixing pot of other technical terms and notation, without any sort of motivation or examples to put them in context. There's no intuition behind them. There's no frame of reference. So then of course the final proof of the unsolvability by radicals of a general quintic just feels like word and symbol soup that you have to learn by rote, because how could anyone possibly have derived it in any sort of deliberate or systematic way? And worse, not only does this result become "magic", the student lacks the ability to use the mathematical tools that support the result for any other purpose either.
Earlier quoted context omitted.
I think the GP is trying to say that, once you get past all of the definitions and proofs, the underlying idea is almost always relatively simple. I do agree that it's pretty hard to be rigorous without setting up all of this edifice, but I've also found that it's very easy (at least, as an applied mathematician) to take an idea and continue generalizing it until the original application becomes a very small corollar…
People will complain about that too. The introduction is "redundant" or "trivial". The book is a long, bloated slog. (Since what you're proposing will unavoidably increase the page count.) The author intentionally confuses students by alluding to some "main theorem" but waiting a hundred pages to say what it is, instead of putting it in front where it belongs. For every complaint about a textbook, there is an equal a…
Some people will, but they probably aren't the target audience for the book, and most people won't.
You don't teach kids who are learning to count about 0 by explaining group theory and identity elements.
Earlier quoted context omitted.
So I find this interesting, because it seems to confirm a suspicion I held. I "only" did some undergrad math during my computer science (but due to a lack of specialization at my university back then it was "real math", i.e. we took the same courses as the math students). My impression often was that a lot of this stuff isn't so hard if you "get to it", but it's clouded in a lot of complicated language that makes it…
Absolutely. It's a problem with academia in general. Academics don't get rewarded for explaining things in an easy to understand way. Moreover, it is often a huge amount of work to distill results down like this. And if you succeed the response you may get is "well that is obvious". Anyway, this is my counter argument to the "formalization of mathematics": why don't we incentivize people to bring some clarity to the…
e.g. look at this advice from the academia stackexchange, to a young aspiring mathematician:
"If you're relatively young and inexperienced and hoping for best results on the rapid publication of your work in strong journals, I would stick pretty mercilessly to the format: (i) strong introduction motivating your work and explaining clearly the value added both in the results themselves and the techniques of proof and (ii) the rest of the paper contains careful proofs of all the results, in a very clear, linear, easy to follow fashion, e.g. "Section A.B: Proof of Lemma C".
Earlier quoted context omitted.
The above statement is true with the assumption that the topic being discussed is truly above the level of understanding for undergraduates. For the majority of the papers, that assumption is not true though. Papers are hard to read has more to do with the idea that if it's not filled with jargons, its chance of getting published is greatly reduced. Papers are not rewarded for being easy to understand. People/organiz…
Depends on the field. Many CS papers can be understood by undergrads because CS is a very young and very broad field; the path to the frontier in any direction is short. Theoretical physics and math are not like that. They have been building cumulatively for centuries.
For state-of-the-art research in obscure specialisms, of course you're right.
However, numerous papers and books cover more mundane subjects and there is no good reason they could not be readily accessible to anyone with an undergraduate-level background or at least a masters delving a bit deeper into the field of interest. Often the problem isn't dumbing down the material, it's simply poor communication skills.
Put another way, while our cumulative understanding of mathematics now covers a very broad range of areas, that doesn't necessarily mean the depth to reach a good understanding of any particular specialism has increased at the same rate. On the contrary, given that even the most specialised of theories must be something that an individual can come to understand and build upon within a single career, there is an inherent limit to how deep our understanding of the subject can go. That limit fundamentally depends on how efficiently we can build the layers of more elementary understanding on which the start of the art must rest.
Earlier quoted context omitted.
But, more consistent with the alarmist headline: > “I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,” Buzzard told Motherboard while he was attending the 10th Interactive Theorem Proving conference in Portland, Oregon, where he gave the opening talk.
Someone who says that is, ironically, not concerned with the details. All of published math is wrong? No, a lot of is is understandable and verifiable by advanced undergraduates. Most of the fundamental theorems in each field are understandable by humans. As you get more and more abstract, and get into more and more obscure areas, you start to see non-understandable proofs built on top of non-understandable proofs. T…