[HN Gopher] Some stuff I found interesting about number theory r...
___________________________________________________________________
Some stuff I found interesting about number theory research
Author : luu
Score : 291 points
Date : 2021-07-26 03:43 UTC (19 hours ago)
(HTM) web link (twitter.com)
(TXT) w3m dump (twitter.com)
| adam_ellsworth wrote:
| What really jazzes me here is this: > "(People learn this stuff
| via the number theory gossip grapevine apparently?)" With the
| panoply of dev-oriented social platforms I find it curious that -
| to my knowledge - nobody who's studied Number Theory, Category
| Theory, Set Theory, etc. have established a kind of social
| network for sharing ideas formally. Between LaTeX for Markdown
| and the limitless Compsci-leaning Maths experts you'd think there
| would be a thriving online community out there! I only have an
| undergrad's (very limited) understanding of these topics but feel
| the ability to create a network for effective communication on
| these topics is 100% doable. (Isn't this the kindof thing the DAT
| and IPFS protocols were supposed to solve? P2P protocols/networks
| for bettering communication?)
| z77dj3kl wrote:
| The social networks are offline. Universities are great at open
| collaboration, it's just not a kind of online collaboration
| where anybody can walk in and partake. People spend a lot of
| time on a different type of communication: going to
| conferences, attending seminars, and meeting one-on-one. Why
| should it be online?
|
| Also keep in mind that a lot of mathematicians are also older,
| less tech-savvy. This might change in the next decade or two!
| d0mine wrote:
| > Why should it be online?
|
| Compare programming before and after Google or before and
| after StackOverflow.
|
| There is https://mathoverflow.net/
| benrbray wrote:
| I do wonder where all the mathematicians / academics hang out
| online. Now that I'm out of (compsci) grad school, I find
| myself without like-minded peers to study math with. Currently
| working my way through Riehl's category theory book, but it's a
| bit tough without anyone to talk to!
|
| I know there's MathOverflow, and some people in the FP
| community hang out on IRC. What's the academic equivalent of
| HN? GitHub? I'm guessing there must be quite a few hard-to-find
| Discords for specific research communities.
| renewiltord wrote:
| An ex-girlfriend of mine is a mathematician. Mostly
| conferences and symposia. It's a very meatspace activity. I
| haven't kept in touch but the pandemic might have upended
| that.
|
| I'd speculate that it's because it's hard to understand much
| of mathematics without the back and forth of a lecture to
| help. But that could just be because I truly suffered through
| my Mathematics graduate degree and am glad a Masters is all I
| managed.
| williamstein wrote:
| One answer to "What's the academic equivalent of HN?" is
| "going to week-long conferences and workshops", which often
| involves a bunch of presentations of papers (with Q&A) and
| discussions long into the night. Before the pandemic, an
| academic (such as me) could easily spend the entire summer
| just going from one conference to another. With the pandemic,
| there's now a lot of live video chat, and seminar series
| where everybody gets together in Zoom, there's a talk, and
| discussion afterwards. Here's an example of such a series for
| number theory: https://sites.google.com/view/vantageseminar
| And, here's a massive list of mathematics (and related)
| online seminars: https://researchseminars.org/
|
| In math there's also a lot more "think deeply and send an
| email" that happens, rather than things like Hacker News.
| bakuninsbart wrote:
| > In math there's also a lot more "think deeply and send an
| email" that happens, rather than things like Hacker News.
|
| That would have been my guess, too. I shared an office for
| a while with a math professor, and he spent around half of
| his time in the office writing emails to colleagues.
| throwaway81523 wrote:
| There is mathoverflow.net and its meta site as math researcher
| hangouts, plus ncatlab.org for category theory, and various
| sites, blogs, mailing lists etc. for other fields.
|
| You might also like Bill Thurston's famous article "On Proof
| and Progress in Mathematics", which says not so much that math
| is social, but that human mathematicians want personal
| understanding of mathematical truths. So black box computer-
| checked but human-incomprehensible proofs aren't of that much
| appeal.
|
| https://arxiv.org/abs/math/9404236
| linspace wrote:
| A little offtopic:
|
| It's telling how you can tell the article was written by a
| mathematician, apart from the obvious fact that it's about
| mathematics. I'm talking about the structure. For example:
|
| "How do mathematicians prove theorems? This question
| introduces an interesting topic, but to start with it would
| be to project two hidden assumptions:
|
| (1) that there is uniform, objective and firmly established
| theory and practice of mathematical proof, and
|
| (2) that progress made by mathematicians consists of proving
| theorems"
|
| It reminds me of a joke I was told by my math teacher when I
| was at school about how mathematics shapes your thought (I
| may do a poor translation):
|
| An air balloon traveller encounters very dense mist and gets
| lost and so is forced to descend to the ground, where he
| finds a guy taking a walk. The traveller asks the guy "Excuse
| me sir, could you tell me where am I?" The guy, after a very
| long pause answers "You are on a balloon". The traveller
| smiles and says "You are obviously a mathematician". "How do
| you know?" asks the guy to which the traveller replies.
| "Easy, there are three very good reasons. The first one is
| that you took a long time to answer, obviously considering
| just the facts and proceeding with strict logic. The second
| one is because the precision of your answer. And last but not
| least because your answer is useless"
| throwaway81523 wrote:
| You can also tell that the article was written by a
| mathematician by noticing that the author is Bill Thurston,
| a very famous mathematician, who we sadly lost a couple of
| years ago. He was amazing. I guess it never would have
| occurred to me to identify the writing style as
| mathematician-like in its own right, since I was expecting
| it to be what it was.
| jjgreen wrote:
| A little further off-topic. I knew (well) a mathematician
| who most of the department thought a bit odd, and he was.
| If you asked him "how are you?", he would take longer than
| is usual to respond. I fairly quickly realised it was
| because he considered that nicety as an actual question and
| gave a considered response.
| jkhdigital wrote:
| I do the same thing! Should've been a mathematician I
| guess...
| webmaven wrote:
| There are variatons on this joke that are even more apropos
| to HN, for example:
|
| A man is flying in a hot air balloon and realizes that he
| is lost. He reduces height and spots a man down below. He
| lowers the balloon further and shouts, "Excuse me. Can you
| help me? I promised a friend I would meet him half an hour
| ago, but I don't know where I am."
|
| The man below says, "Yes. You are in a hot air balloon,
| hovering approximately 30 feet above this field. You are
| between 40 and 42 degrees north latitude, and between 58
| and 60 degrees west longitude.
|
| "You must be an engineer" says the balloonist. "I am",
| replies the man. "How did you know?"
|
| "Well..." says the balloonist. "Everything you told be was
| technically correct, but I have no idea what to make of
| your information and the fact is I am still lost."
|
| The man below says, "You must be a Manager"
|
| "I am", replies the balloonist. "How did you know?"
|
| "Well..." says the man. "You don't know where you are, or
| where you are going. You made a promise which you have no
| idea how to keep, and you expect me to solve your problem.
| The fact is you are in the exact same position you were in
| before we met but now it is somehow my fault."
| madcaptenor wrote:
| That answer isn't even technically correct unless the man
| on the ground is in a boat: https://www.google.com/maps/p
| lace/42%C2%B000'00.0%22N+60%C2%...
| foxes wrote:
| https://threadreaderapp.com/thread/1419281153983500290.html
| eterevsky wrote:
| I always wonder why would someone write a thousands-words
| article as a Twitter thread? Why not publish it on any other
| platform and link it?
| arn wrote:
| Prob a few reasons. This was written in a very conversational
| tone.
|
| If he wrote it in a blog, it would read weird or he'd spend a
| lot more time on it. I've started blog posts before and just
| kinda gave up when it didn't seem like it came together well.
| etaioinshrdlu wrote:
| It would be nice if we had a mathematics-wide push for formal
| verification of proofs, not just done by the mathematicians who
| really like formal verification. Maybe there could be a journal
| of only formally-verfified results?
| jkhdigital wrote:
| Homotopy type theory is just that:
| https://www.ias.edu/ideas/2014/voevodsky-origins
| deadbeef57 wrote:
| Homotopy type theory (HoTT) can mean several things: it's a
| new foundation of mathematics that was developed from the
| start with computer-formalization in mind. But you can also
| work on HoTT without ever touching a computer.
|
| Conversely, there are many ways to do computer-formalization
| of mathematics, without every doing anything with HoTT.
| Someone wrote:
| https://sciendo.com/journal/FORMA gets close, I think (I don't
| think it _only_ publishes formally verified results. It likely
| also accepts more philosophical texts about formal
| verification). There's also http://mizar.org/JFM/
|
| I don't think such journals can be the full solution, though.
|
| Problem is that to entice mathematicians who don't like formal
| verification to publish in it.
| z77dj3kl wrote:
| What do you mean? Mathematics _is_ all about formal
| verification, i.e. proofs.
| SAI_Peregrinus wrote:
| I think they mean computer-verified proofs. As you note, the
| existing proofs are already formally verified, so this might
| not add much.
| dash2 wrote:
| This reminds me of my favourite description of academic research,
| from _To the Lighthouse_ :
|
| "For if thought is like the keyboard of a piano, divided into so
| many notes, or like the alphabet is ranged in twenty-six letters
| all in order, then his splendid mind had no sort of difficulty in
| running over those letters one by one, firmly and accurately,
| until it had reached, say, the letter Q. He reached Q. Very few
| people in the whole of England ever reach Q. Here, stopping for
| one moment by the stone urn which held the geraniums, he saw, but
| now far, far away, like children picking up shells, divinely
| innocent and occupied with little trifles at their feet and
| somehow entirely defenceless against a doom which he perceived,
| his wife and son, together, in the window. They needed his
| protection; he gave it them. But after Q? What comes next? After
| Q there are a number of letters the last of which is scarcely
| visible to mortal eyes, but glimmers red in the distance. Z is
| only reached once by one man in a generation. Still, if he could
| reach R it would be something. Here at least was Q. He dug his
| heels in at Q. Q he was sure of. Q he could demonstrate. If Q
| then is Q--R--. Here he knocked his pipe out, with two or three
| resonant taps on the handle of the urn, and proceeded. "Then
| R..." He braced himself. He clenched himself.
|
| Qualities that would have saved a ship's company exposed on a
| broiling sea with six biscuits and a flask of water--endurance
| and justice, foresight, devotion, skill, came to his help. R is
| then--what is R?
|
| A shutter, like the leathern eyelid of a lizard, flickered over
| the intensity of his gaze and obscured the letter R. In that
| flash of darkness he heard people saying--he was a failure--that
| R was beyond him. He would never reach R. On to R, once more. R--
|
| Qualities that in a desolate expedition across the icy solitudes
| of the Polar region would have made him the leader, the guide,
| the counsellor, whose temper, neither sanguine nor despondent,
| surveys with equanimity what is to be and faces it, came to his
| help again. R--
|
| The lizard's eye flickered once more. The veins on his forehead
| bulged. The geranium in the urn became startlingly visible and,
| displayed among its leaves, he could see, without wishing it,
| that old, that obvious distinction between the two classes of
| men; on the one hand the steady goers of superhuman strength who,
| plodding and persevering, repeat the whole alphabet in order,
| twenty-six letters in all, from start to finish; on the other the
| gifted, the inspired who, miraculously, lump all the letters
| together in one flash--the way of genius. He had not genius; he
| laid no claim to that: but he had, or might have had, the power
| to repeat every letter of the alphabet from A to Z accurately in
| order. Meanwhile, he stuck at Q. On, then, on to R."
| nullc wrote:
| > Anyway, despite the fact that error-correction is really hard,
| publishing actually false results was quite rare because
| "people's intuition about what's true is mysteriously really
| good."
|
| I don't find that mysterious. One aspect of number theory is that
| results have arbitrarily deep implications and relations. If you
| are wrong about something you can often substitute it in
| somewhere else and produce a wrong answer or a contradiction.
|
| Doing something wrong which still looks right after being tested
| from a few different perspectives is extremely tricky.
|
| Like finding a pseudoprime for some probabilistic primaility
| test-- it's not likely to also be a pseudoprime for an unrelated
| test. So pretty much the only way to pass a collection of
| independent probabilistic tests is to actually be prime. (Note
| the 'pretty much'-- a bunch of approximate proofs isn't a
| necessarily proof, but it at least explains why false things are
| seldom believed even when their headline proofs aren't solid)
|
| I don't just mean through different reviewers -- when you publish
| a proof of something you've probably satisfied yourself that it
| was true through multiple avenues. The proof you published was
| just the one you thought was the most convincing. Unfortunately,
| making an error in it can be something that makes a proof more
| convincing (until the error is found), but fortunately having an
| incorrect proof of something doesn't make the underlying fact
| untrue.
| renewiltord wrote:
| I wonder if they have the equivalent the engineers who bemoan the
| fact that some React developers make functioning websites without
| "knowing anything about how CPUs or memory models work".
|
| Bourbaki was a thing so probably. And we know the joke about
| Bourbaki and Lang. Though the reference is diminished by the
| latter's relationship with the former.
| laichzeit0 wrote:
| It's higher than that. People build software calling .search()
| and .sort() after a 4 month nanodegree and don't know how to
| implement either. I'd say they are even using http requests
| without knowing what a TCP socket connection is, maybe even
| what an http request header is. The barrier to entry in the dev
| world is extremely low.
|
| To relate it to maths: It would be equivalent to someone doing
| math research without knowing how to do proof by induction (in
| analogy to not knowing how to implement .sort())
| Isinlor wrote:
| Lack of gatekeeping and general accessibility of software
| development is the beauty of this profession.
| laichzeit0 wrote:
| Sorry, let me rephrase. I didn't mean it in a negative way.
| The last time I needed to actually implement a sort method
| was when I was doing very low level embedded work and there
| wasn't one available on that platform (at least not one
| with the memory/compute trade offs I needed). I'm
| sympathising with mathematicians who have to build stuff on
| black-box stuff they don't full understand. Things are too
| complex to know it down to the CPU level, even so complex
| that modern devs don't even know how search and sort is
| implemented, but still get shit done.
| hnfong wrote:
| I'm not a mathematician, but in the rare occasion I have to
| use the Pythagoras theorem, I use it without knowing how to
| prove it.
|
| And that's OK.
|
| (Mathematicians are probably too polite to moan about amateur
| plebs like me who didn't even learn primary school
| mathematics properly)
| wbl wrote:
| Behold!
| http://www.geom.uiuc.edu/~demo5337/Group3/Bhaskara.html
|
| It's so pretty everyone should know it.
| lyaa wrote:
| These devs don't need to. As long as they get work done,
| create `value', their skills are sufficient. Admittedly,
| there are times when people who know better are needed for
| specific tasks and that's why we are paid better.
|
| Proof by induction is more akin to for-loop than optimized
| sort algorithms. It's often taught in the first mathematics
| course that includes proofs which can be Calculus II or even
| Linear Algebra. I would be surprised if a Math student did
| not learn it by their first Analysis course.
| regularfry wrote:
| It's funny, I'd say that the reason these devs don't need
| to understand the lower layers is because the layering
| abstraction was built well enough. That's a good thing!
| achenet wrote:
| I'm afraid I don't know the joke about Bourbaki and Lang, could
| you please share it?
|
| I do have a possibly relevant joke: A math student asks his
| professor how to visualize a result in 7-dimensional space. The
| professor responds: "It's easy. I visualize the result in
| n-dimensional space, then simply take n = 7."
| mathieubordere wrote:
| https://www.reddit.com/r/math/comments/j569y/can_someone_exp.
| ..
| z77dj3kl wrote:
| I've heard of mathematicians being frustrated by physicists who
| use fancy stuff without full understanding of the underlying
| principles, and sometimes they just manipulate the notation
| without fully justifying what that manipulation means (e.g. you
| may have an integral operator on some space, and you might just
| swap an infinite sum and that integral operator, but that
| requires a justification that you might omit).
| benrbray wrote:
| This is quite interesting, especially since one of the major
| objections to computer-aided proofs has that they are more
| difficult for humans to understand.
|
| Common wisdom has been that proof techniques matter more than the
| results, but if human-authored proofs are no longer being
| inspected, it seems like it's just a matter of time before
| computer-aided proofs take over. I wonder how long it will be
| before proof assistants (like Lean, Coq, etc.) become ergonomic
| enough that the average non-technical math researcher will feel
| social pressure to publish a computer-aided proof along with
| their result.
| jkhdigital wrote:
| 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.
| alexilliamson wrote:
| He's been dead for four years?
| dhosek wrote:
| Apparently he didn't shut down his computer before he died.
| queuebert wrote:
| Dat uptime tho
| jkhdigital wrote:
| Oh snap, I had no idea that he died! Wow... that's a
| profound loss for the field of mathematics.
| aaronlevin wrote:
| The main objection to computer-aided proofs is not that they
| are more difficult for humans to understand.
|
| The main objection is that most proof-assistants use a
| different logical foundation than modern mathematics. Modern
| mathematics is built on ZFC[0] whereas most proof assistants,
| such as Coq, Isabelle, Agda, etc use different logical
| foundations, such as the Calculus of Constructions[1].
|
| Many important results in modern mathematics are not easily
| stated or proven in systems such as CoC[1]. For example,
| Brouwer's _Fixed Point Theorem_[2], a pretty bog standard
| result in Topology that is useful to proof many things in
| Functional Analysis, has a clear statement in ZFC, but does
| not, to my knowledge, have an equivalent in CoC (and if it does
| it will be stated radically different).
|
| [0]:
| https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
| [1]: https://en.wikipedia.org/wiki/Calculus_of_constructions
| [2]: https://en.wikipedia.org/wiki/Brouwer_fixed-point_theorem
| plake wrote:
| 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 a skilled
| mathematician, and invite them to fill in the lower-level
| details themselves. This reasoning is as much intuitive as it
| is formal; I suspect it will be a while before proof assistants
| are as intelligent as the typical reader of a mathematics
| paper.
|
| I think there's an outside perspective that if math isn't 100%
| logically verified, it's worthless, which doesn't really match
| up with my own experience. Most results rely more on the
| intuition of the authors than on the precise logic they write
| down; thus the surprising result that papers with logical gaps
| are, very often, still correct.
| benrbray wrote:
| 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?
| plake wrote:
| 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.
| daxfohl wrote:
| I came here to say that maybe it makes things simpler
| though when everyone speaks the same language, and all
| proofs are written in the same format.
|
| However then I remembered the new codebase I inherited
| and OMG it's such a mess because somehow just converting
| a UI enum to a DB enum is a 25-line function that's
| repeated over and over everywhere. (Needs to be version-
| safe for different clients that may have old enum values,
| needs to create error message in appropriate language,
| etc, and the callers are in different layers and all have
| different ways of getting the corresponding info).
|
| So yeah maybe the high-level "I get it, you get it, we
| all get it, let's just state this an move on" is better.
| williamstein wrote:
| I 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). When I was a grad student
| at Berkeley, I once asked Serge Lang (who I think wrote the most
| advanced math textbooks of anybody who ever lived) why
| mathematics research papers don 't have a lot more incorrect
| results in them. 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. Of
| course, there are serious mistakes and gaps in the literature,
| though what one person considers a gap, somebody else who knows
| more might not consider a gap. For example, I remember once that
| Ernst Kani was complaining to me about a big gap in a paper by
| Ribet; I didn't believe it, so I read the relevant section and
| was able to fill in the gap in a few hours sufficiently to
| satisfy him. In any case, I've spent decades both programming and
| doing number theory, and despite some similarities, they are very
| different things. Another related way these threads come together
| is with Kevin Buzzard's big project to formalize mathematics
| using LEAN; he's another number theorist, and he told me that a
| few years ago he started really worrying about the correctness of
| a lot of number theory papers, and that strongly motivated his
| interest in LEAN.
| oolonthegreat wrote:
| 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
| hyperbovine wrote:
| > 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 your name to it sending it
| out the door. Also most mathematicians are extremely averse to
| even _saying_ something that 's incorrect, let alone putting in
| print. There's ton of sanity-checking and trying to break your
| own result that, again, is rarely if ever mentioned in the
| final publication.
| caddemon wrote:
| 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?
| concreteblock wrote:
| I think it's fundamentally a question of incentives. A
| mathematician's career prospects and status depends heavily
| on being able to prove things that others can't. Why spend
| extra time helping your 'competitors'? Not saying this is
| ideal, but it seems to explain many behaviours in the
| community, and it seems unavoidable given the ever-
| increasing competition for jobs.
| andai wrote:
| It does seem like including a few alternative proofs would
| greatly aid in understanding.
| thehappypm wrote:
| It's actually pretty tough to write out a proof, and going
| from a whiteboard where you're 99.9% sure it's right to
| something in LaTeX in a paper in your field is actually a
| long number of steps to take.
| shuckles wrote:
| During an undergraduate research program, I discovered a gap in
| a theory in PDEs which I'm assuming nobody else did because I
| was the only one who tried to follow each step (just getting
| that far was the entire purpose of the effort!). My advisor
| said it would be best to fix the gap before publishing about it
| because multiple students entering the job market depended on
| the result being true. That was an eye-opening social
| experience.
| lcq92 wrote:
| Can you share what the gap was?
| gameshot911 wrote:
| So were you able to fix it??
| redtexture wrote:
| Partial Differential Equations for the rest of us.
| jkhdigital wrote:
| 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
| mhh__ wrote:
| 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.
| jkhdigital wrote:
| I'm a PhD student in computer science, and after spending
| some time on this subject I'm pretty well convinced that
| parts of mathematics and CS are converging towards a more
| unified foundational framework that will benefit both
| fields tremendously.
|
| In a nutshell, the key challenge is taking the core of
| complexity theory (which is easy to formalize in terms of
| state machines) and migrating it into the language(s) of
| category/type theory (which is much more
| modular/compositional).
|
| A couple interesting recent works in this area:
|
| _Categorical Complexity_ :
| https://www.cambridge.org/core/services/aop-cambridge-
| core/c...
|
| Dusko Pavlovic's _Monoidal computer_ series: 1.
| https://arxiv.org/pdf/1208.5205 2.
| https://arxiv.org/pdf/1402.5687 3.
| https://arxiv.org/pdf/1704.04882
| mhh__ wrote:
| I mostly hope you're right, good luck. Post your thesis
| here when the time comes.
|
| I'm a bit of a philistine when it comes to cutting edge
| CS in this area so I'll leave you to it!
| pramodbiligiri wrote:
| When you say that state machine problems are basically
| solved, are you referring to any tools that you're using to
| reason about them?
| mhh__ wrote:
| By solved I really mean "in commercial use", there's
| probably a lot of research let to be done, but people are
| already verifying TLA+ specs all day everyday.
| [deleted]
| [deleted]
| CJefferson wrote:
| I find the further off the "main path" you go, the easier it is
| to find incorrect papers.
|
| In particular, I found a few papers which claim to provide
| algorithms which solve some problem. If there is no evidence
| the algorithm was ever implemented, there is a distribingly
| good chance it doesn't work -- I used to sometimes give such
| papers as projects for students, but now I always start on day
| 1 saying "Be prepared for this to be wrong".
| nicoburns wrote:
| > 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.
| ska wrote:
| There is a fundamental tension here because a) doing this
| stuff properly takes a long time and b) lots of undergraduate
| math teaching is "service" teaching, meant to get students up
| to a level where they can do the manipulations needed in
| other courses.
|
| This is why there is typically separate Calculus and Real
| Analysis streams in undergraduate - the former is needed for
| all the hard sciences and engineering, the latter for math
| students and fellow travelers who really want to understand
| what is going on and be able to prove things properly.
|
| Typically the analysis stream will start with a pretty in-
| depth look at what real numbers actually are (spoiler:
| weirder than you thought) and the implications of that. You
| get a much better understanding this way but you don't cover
| ground nearly as quickly.
| smallnamespace wrote:
| Knowing and using a thing and proving it are (usually)
| different skills.
| hannob wrote:
| 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".
| Sniffnoy wrote:
| This[0] may be a good place to start, but I'm not sure if it
| contains proper examples of what you say (of serious
| collapse). E.g., I expect a lot of people probably relied on
| the false result mentioned by Matheus, but most of them could
| probably be repaired with the corrected statement. So it
| seems like this probably hasn't happened?
|
| OTOH, there was the Italian school of algebraic geometry, but
| that was more than one single flaw...
|
| [0] https://mathoverflow.net/questions/35468/widely-accepted-
| mat...
| dynrzk wrote:
| Somewhat famously, symplectic geometry had its fair bit of
| foundational issues.
| Penyngton wrote:
| 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 Godel 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 Godel'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 Borger, Gradel 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.
| jkhdigital wrote:
| Obligatory pointer to homotopy type theory:
| https://www.ias.edu/ideas/2014/voevodsky-origins
| RajuVarghese wrote:
| In a book on mathematics by Alex Bellos he says that any
| contemporary cutting-edge research mathematics paper can be
| understood by no more than 100 mathematicians. The field is
| getting bigger and bigger and there are less and less
| mathematicians that have background knowledge sufficient to
| _understand_it much less critique it. The bar for the word
| 'understand' may be much higher in mathematics compared to other
| fields. Comments?
| Agingcoder wrote:
| Not really.
|
| There's 'understand', and 'believe you understand', and in
| other fields (say, software engineering...) you meet lots of
| people who think they understand, when they don't. I also think
| that in the SE case, because it's more 'relatable' ('look at my
| website') , people generally assume more easily that they
| understand when they don't.
|
| Also if you look at theoretical comp sci results (calculability
| theory, etc) , or even complex software engineering systems
| (actual working distributed systems, etc) , I very much doubt
| that many people (apart from the people who designed and wrote
| them, and who may even be wrong about them! ) can _actually_
| claim to understand them fully. You will understand, to some
| extent, the 'theorem' (ie the system), but the implementation
| will remain a black box.
| onion2k wrote:
| That sounds like something that'd be true for _every_ field,
| not just math. The nature of anything that 's cutting edge
| means very few people will have looked at it yet let alone
| actually understood it.
| RajuVarghese wrote:
| I agree that the number of people that can understand a
| cutting-edge paper will be low. But, in CS for example, the
| number will be much higher than 100. I would assume that it
| would be in the 1000's worldwide. Since, it isn't my field I
| could speculate that cutting-edge biology would be understood
| by a _lot_ more than 100 persons.
| Hermitian909 wrote:
| I think the main thing missing from this analysis is how much
| of the mathematical corpus ends up being "uninteresting" over
| time.
|
| Take Algebraic Geometry, a field primarily concerned with the
| question "what are the zeroes of multivariate polynomial
| equations" e.g. x^2-y+z^3. Papers that could be considered part
| of the field were published as early as the 16th century but
| very little is worth reading from before the work of Alexander
| Groethendieck in the mid 20th century which really formalized
| the field in the form it is today. The vast improvement in
| abstractions meant old proofs could be rewritten in a much
| terser, easier to understand manner with the new machinery.
|
| Similarly, now that we've solved the classification of finite
| simple groups[0] a lot of the deep expertise mathematicians had
| surrounding techniques to classify finite groups is no longer
| needed. A new researcher can learn a small, curated subset of
| these techniques and fully grasp the field. Since there's no
| more work to be done, there's no need to build deep intuitions.
|
| More generally a _lot_ of papers in mathematics are attempts to
| build the machinery to solve some bigger problem and most of
| those end up not being useful when the field cracks said
| problem. At which point, all those papers effectively get
| "trimmed away" since the result they were meant to support does
| not depend on them, and so no one need read them.
|
| [0]
| https://en.wikipedia.org/wiki/Classification_of_finite_simpl...
| deadbeef57 wrote:
| I just want to say that in the case of the classification of
| finite simple groups, there's actually a bit of a problem.
| Exactly because "a lot of the deep expertise mathematicians"
| have left the field; but on the other hand "a small, curated
| subset of these techniques" is still missing. A small group
| of experts (all in their 70's or 80's) are currently writing
| a dozen volumes on this classification, and the rest of the
| community hopes that they get it done before they pass away.
|
| This proof has a seriously low bus factor at the moment
| :scared:
| Hermitian909 wrote:
| Oh you're right! I hadn't been aware that the book series
| was incomplete, my face is a bit red and I share your
| concerns. Here's to hoping!
| daxfohl wrote:
| In a way that's what makes the question of AI math
| interesting. _Probably_ AIs will be better than us at math in
| a couple decades. But that might not change anything because
| it 's still up to humans to determine whether a result is
| interesting. And it may take us just as long to understand
| AI-created concepts as to build them up ourselves. Maybe math
| starts looking more like archaeology at that point. (Though
| it's arguably archaeology anyway -- the proofs are all "out
| there", we just have to find them).
| yellowcake0 wrote:
| There is no way that AI will be better than us at math in a
| couple of decades.
| Y_Y wrote:
| I like this idea. People often ask if maths is "created" or
| "discovered". Maybe we can say that it's "excavated" and
| that we know it's down there somewhere, we just need to put
| in a few years of shoveling.
| thaumasiotes wrote:
| > (I suggested that perhaps this is because the famous people are
| the only ones who are fast enough to actually do everything
| you're "supposed to do" and still be productive.)
|
| I might suggest that these are broadly the set of people who are
| _able_ to understand the proofs, and that their higher ability
| also causes them to produce higher-quality work, so the fame and
| the understanding are separate effects of a root cause. (With
| understanding then feeding into fame.)
|
| I don't buy that spending time understanding the material you're
| working with takes time away from producing results. They are
| complementary efforts, not opposed ones.
| tragomaskhalos wrote:
| Maths is, I believe, unique as a discipline in that it displays a
| distinct set of _discrete_ difficulty steps the further into it
| you go. The first step is encountered at school: many students
| find they may be OK with basic arithmetic but anything conceptual
| like algebra is beyond them. A second step is encountered at
| college /university: someone who is perfectly good at school-
| level mathematics can find themselves totally at sea within
| literally week 1 of a degree course. And someone who copes fine
| with this level may in turn find that the more rarefied and
| demanding level demanded by a very top university is beyond them
| (source: this was my own experience - fine at degree level at an
| 'ordinary' university having flamed out spectacularly in an
| Oxbridge interview, demonstrating absolutely that I'd have been
| totally out of my depth there). Then, there are those few who
| push through even that level with enough ability to become
| productive and innovative academics.
|
| When you start with a population for whom even arithmetic can be
| a challenge, it's not too surprising that only a miniscule
| priesthood emerge from the other side.
| petercooper wrote:
| 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.
| themodelplumber wrote:
| One of my takeaways: When I see "stitch together black boxes," to
| me that says that aspects of academic math are becoming similar
| to opportunistic software development.
|
| When such an effect happens in group psychology it is typically
| part of the "grounding" effect happening. There is a high supply
| of theory without the energy to go into analyzing so many
| individual black boxes anymore, and a correspondingly high demand
| arises for integrative applications which bring the high-minded
| ideas down to more fundamental, widely-scoped, or practical
| effect. Down to earth, so to speak.
|
| Some would think of this as an economic-benefit effect. The point
| is, it tends to bring all those stitched-together black boxes
| much closer to the end user space, where application is key, not
| so much theory.
|
| So I wonder if in the coming years we will see a dramatic closing
| of the gap between direct access to mathematics inputs and daily
| living. It may be that the typical non-math-minded individual
| will soon readily and happily bootstrap themselves into the
| language of mathematics via the closing in of a perception of
| direct competitive or economic value.
|
| To share an example, in 2003 I started to use a node-based editor
| to edit 3D textures for graphics projects. This node-based tool
| gave more control than standard sliders, color pickers, and
| checkboxes. But soon I discovered that in a lot of cases it was
| easier to enter a math formula in a node than to chain nodes
| together. Maybe a single checkbox designated whether the function
| was periodic, but other than that, enter math here, please. Your
| mathematical wish is our graphics-producing command.
|
| So I wonder if we'll soon get to the point where formulaic
| systems control with direct mathematic input will be more
| desirable and common in unified system interfaces that are found
| in office and household work.
|
| Let's say you want to write the perfect formula for a given air
| quality factor in your office...
|
| Or your competitive game which allows you to program AIs is made
| much more efficient if you can tweak formulae by hand...
|
| Or you need to design a new form of printed steak, but simple
| toggles and switches just won't do...
|
| (Then...when the time is right for the black-box theory end to
| pick up a lot of momentum again, imagine how large a pool of new
| mathematicians will be ready...)
| rocqua wrote:
| I think the reason for this black-boxing in software and
| mathematics is quite different.
|
| In top-level mathematics its that you have no choice but to
| treat results as black-boxes because the complexity otherwise
| is just too high. Its the only way forward, and mathematicians
| would prefer not to take this approach.
|
| In software development, black-boxing is a way of accelerating
| development. It allows people to abstract away and disregard
| complexities. And it allows re-using big works. It comes at the
| cost of some integration losses and performance losses. But,
| since they are not at the complexity limit, software developers
| can dive into their black boxes if required for performance or
| other reasons.
| webmaven wrote:
| But "accelerating development" and "lowering complexity" are,
| if not synonymous, then at least highly correlated.
| rocqua wrote:
| The difference is in why. Mathematicians do it out of
| necessity because they are at the edge of complexity they
| can handle. Developers do it because it is convenient.
| Developers have a choice.
| webmaven wrote:
| I think you may be underestimating how much "because they
| are at the edge of complexity they can handle" is a
| driver of mainstream SE. In particular, as a factor in
| the popularity of frameworks and libraries.
|
| I'm not taking a stance like "if it was hard to write it
| should be hard to use", but quite a lot of software only
| seems to exist in order to hide complexity away in black
| boxes, often in trivial ways.
| jaksmit wrote:
| If anyone is interested in number theory and would like to help
| some incarcerated people that are working on a number theory
| paper:
|
| I'm a director of the Prison Math Project:
| http://prisonmathproject.org/
|
| We have a few advanced mathematicians in jail who don't have
| access to computers. They need help with formatting their work in
| LaTeX and stuff like that to make it ready for publication
| (credit offered).
|
| They have previously co-authored some papers from within jail eg
|
| "Linear Fractional Transformations And Nonlinear Leaping
| Convergents Of Some Continued Fractions"
|
| "Math And Art In Prison: A Collaborative Effort Across The Ocean"
|
| please reach out if any interest in helping them.
| soheil wrote:
| > except that for programmers it's possible (and advantageous
| IMO) to deeply understand way more than they actually do, which
| seems less clearly true in number theory.
|
| But that's not true for programmers either. How often do we look
| at the compiler or interpreter and check each opcode to make sure
| the right transistor gets turned on at the right time? The fact
| that number theory papers are 50-100 pages long may be an
| indication they're missing some useful level of abstraction, but
| then again if they're already operating at the most abstract
| level limited by the human mind then maybe that's why the papers
| are so long.
| rwallace wrote:
| > I suggested that perhaps this is because the famous people are
| the only ones who are fast enough to actually do everything
| you're "supposed to do" and still be productive.
|
| Conjecture: it is instead or also because famous people are the
| only ones who are given enough slack to be able to take the time
| to actually do everything you're supposed to do.
|
| Proposed test to distinguish between the conjectures: do famous
| mathematicians become famous _by_ finding gaps, or find gaps
| _after_ becoming famous?
| echopurity wrote:
| It's a huge failure of the (mis)education system that almost no
| one learns math.
| defterGoose wrote:
| I've been thinking a lot recently about math curriculum and how
| i think students would be well served by an earlier injection
| of set theoretical topics. At once more abstract and yet
| possibly more concrete for many of the "never-math" brains one
| encounters in a typical school setting.
___________________________________________________________________
(page generated 2021-07-26 23:01 UTC)