Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Some stuff I found interesting about number theory research

twitter.com

Post reply on HN
Print view View original

41–50 of 118 posts

Re: Some stuff I found interesting about number theory research

#41

Post by hyperbovine »

williamstein wrote: post #6

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). 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 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.

Re: Some stuff I found interesting about number theory research

#42

Post by z77dj3kl »

etaioinshrdlu wrote: post #14

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?

What do you mean? Mathematics is all about formal verification, i.e. proofs.

Re: Some stuff I found interesting about number theory research

#43

Post by z77dj3kl »

renewiltord wrote: post #10

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.

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).

Re: Some stuff I found interesting about number theory research

#44

Post by z77dj3kl »

adam_ellsworth wrote: post #2

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 exp…

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!

Re: Some stuff I found interesting about number theory research

#45

Post by jkhdigital »

williamstein wrote: post #6

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). 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

Re: Some stuff I found interesting about number theory research

#46

Post by jkhdigital »

benrbray wrote: post #5

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 assist…

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.

Re: Some stuff I found interesting about number theory research

#47

Post by jkhdigital »

etaioinshrdlu wrote: post #14

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?

Homotopy type theory is just that: https://www.ias.edu/ideas/2014/voevodsky-origins

Re: Some stuff I found interesting about number theory research

#49

Post by jkhdigital »

jjgreen wrote: post #34
linspace wrote: post #26

Earlier quoted context omitted.

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 pr…

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.

I do the same thing! Should’ve been a mathematician I guess…

Re: Some stuff I found interesting about number theory research

#50

Post by alexilliamson »

jkhdigital wrote: post #46
benrbray wrote: post #5

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 assist…

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?
Post reply on HN