You know those videos where an expert explains something complicated at five different levels from school kid up to fellow genius? (Example: https://www.youtube.com/watch?v=eRkgK4jfi6M) I feel like many areas of math would benefit from that, because I barely have a clue what exists, let alone why and where there are advancements in the field.
Some stuff I found interesting about number theory research
51–60 of 118 posts
Re: Some stuff I found interesting about number theory research
#52I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
> He responded that it was because people secretly "proved" everything to themselves in multiple ways, but only wrote up one proof, and it was unlikely that multiple very different reasons for something being true would all be wrong.
This was the most frustrating thing for me when I was studying undergraduate maths. Often a result was just stated, with the reasoning behind how it was generated completely omitted. Good professors would go through all of that, but those seemed to be few and far between. The rest just expected you to work it out (despite not ever being exposed to it or pointed to a good source), or rote memorise the result.
Re: Some stuff I found interesting about number theory research
#53Earlier quoted context omitted.
I think it will be quite some time yet. As a researcher, my objection to computer-aided proofs is not that they're hard to read -- you would of course write a human readable version to go with it -- but rather that they're extremely time-consuming to write. (And writing papers is hard enough already.) A typical research paper is written at a very high level; often steps in the argument will assume the reader is also…
That's basically what I meant by "ergonomics" -- do you think we're still quite far from researchers being able to develop their own "tactics" to automate the sort of reasoning that would normally be "left as an exercise" to the reader of a research publication?
Yeah, "left as an exercise" can mean anything from "this is an undergraduate exercise" to "if you understand both the field and this paper, you could write a different, much longer paper, and we both know this, so let's assume I wrote that one."
It's probably not impossible to build a proof language that makes that kind of thing doable, but I suspect that (a) it would be genuinely difficult to operate it skilfully, much as being a really good developer is difficult, and (b) it would take a huge collective effort on behalf of each research community to prove the foundational results everyone relies on.
Whereas the system we have right now, despite sounding kind of weird to outsiders, mostly works okay? I'm just not sure a switch to formal proofs would be worth the time investment -- or that you could convince the many researchers less interested in tech than myself.
Re: Some stuff I found interesting about number theory research
#54Earlier quoted context omitted.
This is an explicit goal of one of of the creators of homotopy type theory, Fields medalist Vladimir Voevodksy: https://www.ias.edu/ideas/2014/voevodsky-origins Apparently he now uses Coq in his everyday work.
He's been dead for four years?
Apparently he didn’t shut down his computer before he died.
Re: Some stuff I found interesting about number theory research
#55I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
Are you familiar with homotopy type theory? One of its proponents, Fields medalist Vladimir Voevodsky, has stated that his contributions are part of a “personal mission” to bring mathematics into a new age of formal verification [1]. I’d be curious to know how this compares to LEAN. [1] https://www.ias.edu/ideas/2014/voevodsky-origins
[deleted]
Re: Some stuff I found interesting about number theory research
#56I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
Given that you seem to know this space, I have been wondering: Was there ever any major flaw in an important mathematical proof that was taken as a given, and subsequently plenty of papers building on that turned out to be wrong as well?
Like I don't mean "this proof has a gap in its justification, but the thing claimed likely is still true". I mean "we thought someone had a proof for X, but actually later someone else showed X isn't true".
Re: Some stuff I found interesting about number theory research
#57I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
Given that you seem to know this space, I have been wondering: Was there ever any major flaw in an important mathematical proof that was taken as a given, and subsequently plenty of papers building on that turned out to be wrong as well? Like I don't mean "this proof has a gap in its justification, but the thing claimed likely is still true". I mean "we thought someone had a proof for X, but actually later someone el…
I'm not sure if this quite matches your request (I suppose much hinges on the word "important"), but here's a story of a fairly famous and long-standing error: https://www.jamesrmeyer.com/ffgit/godel-error-2.html
Personally, I'd say the fact that someone bothered to discover it was false fifty years after it was published shows its importance.
The short version is that Gödel claimed in a paper that he had an algorithm to determine satisfiability for a certain logic, but the algorithm actually worked for a slightly different logic instead. People basically took Gödel's word for it for fifty years until a logician called Goldfarb found the mistake.
EDIT: As a disclaimer, I don't have any association with or endorsement of the website I've linked to. I found it just now because I needed a source for the story that I've known for many years (I think I first heard it in person, but it's definitely contained in the book `The Classical Decision Problem' by Börger, Grädel and Gurevich). I skimmed the post and it seemed to cover the relevant details, but that's the extent of my knowledge of the site and its contents.
Re: Some stuff I found interesting about number theory research
#58I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
Are you familiar with homotopy type theory? One of its proponents, Fields medalist Vladimir Voevodsky, has stated that his contributions are part of a “personal mission” to bring mathematics into a new age of formal verification [1]. I’d be curious to know how this compares to LEAN. [1] https://www.ias.edu/ideas/2014/voevodsky-origins
I am kind of sceptical of these verified-mathematics projects in the sense that my litmus is whether I could easily verify my workings rather than the proofs I rely upon, but nonetheless I have enormous respect for those doing this work and really hope it comes to fruition.
I really hope this work trickles down to our programming - state machine problems are basically "solved" (for my needs at least), but more complex programs are really hard to prove.
Re: Some stuff I found interesting about number theory research
#59I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
> He responded that it was because people secretly "proved" everything to themselves in multiple ways, but only wrote up one proof. I don't do pure math, but I write the occasional theory paper, and this resonates. So much ends up on the cutting room floor--usually you proved the key result three or four different ways before finding a proof that is actually incisive/aesthetically pleasing/whatever to justify signing…
As a student working on some theory papers, I wish this kind of thing would go in an Appendix somewhere. Is it left out because it's not worth the effort to include compared to the number of people that would actually read it? Or is it something that runs the risk of negative perception by those established in the field?
Re: Some stuff I found interesting about number theory research
#60I did a Ph.D. in number theory, published a few dozen research papers, and have programmed a lot and this post sounds about right to me. I did CS as an undergrad, before doing a math Ph.D., and remember being very surprised that math papers weren't a lot more wrong than they actually are (since computer software is so often full of bugs, and all it takes is one single bug to completely invalidate an entire paper). Wh…
wanted to drop a link to buzzard's very interesting talk https://youtu.be/Dp-mQ3HxgDE starting at 13:00 he talks about that frailness. also loved the bit about "elders" at 40:37