Some stuff I found interesting about number theory research | Hacker News Reader

Some stuff I found interesting about number theory research

twitter.com

348 pointsluu115 comments

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.

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.

So were you able to fix it??

Partial Differential Equations for the rest of us.

Can you share what the gap was?

I could tell you, but it might cost some people their job.

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

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

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?

It does seem like including a few alternative proofs would greatly aid in understanding.

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.

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.

> As a student working on some theory papers, I wish this kind of thing would go in an Appendix somewhere.

For what it's worth, this kind of behavior isn't limited to theory papers. Papers presenting analysis and model development also generally only show the "finished" result, omitting most or all of the bad models, training models, development models, etc. that were used to get to the final result. Same thing with observational papers in astronomy and related fields. There's a lot of work done that builds the authors' confidence in the correctness of the result, but that doesn't lend itself to a clean "story" for the paper or perhaps also ends up being supportive but not necessary to demonstrate a result.

I remember being surprised as a student, to learn that papers aren't narrations of the path to a discovery, but rather a narrative to describe the idea in a compelling (and hopefully clear) fashion.

Oh for sure, I started out doing molecular biology so I dealt with missing methodology details all the time there - certainly some things make sense to leave out, but there were also cases where it took trial and error to replicate because details on intermediate steps were left out.

That is what it is, but in the case of theory I think the alternative proofs could actually be really educational. The exact details of a biology technique (and hyperparameter searching type stuff for that matter) don't have the same inherent interest to me.

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.

When you say that state machine problems are basically solved, are you referring to any tools that you're using to reason about them?

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.

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

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!

Homotopy type theory is a mathematical foundation, like set theory, or Martin Lof's type theory. This is different from a proof assistant like Coq or Lean. In fact, Lean has a library which implements part of HoTT (see https://github.com/leanprover/lean2/blob/master/hott/hott.md). In short, there is no comparison between Lean and HoTT.

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

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.

Knowing and using a thing and proving it are (usually) different skills.

True; but so are understanding a thing well and being able to use it.

I wasn't really talking about proof-based vs. not though - it's true that an analysis course will be more proof based (than Calculus) because that is also a skill you are expected to be developing.

However most calculus graduates, even the ones at the top of their class, still have at best a somewhat superficial understanding of the set of real numbers and functions on it, regardless of whether or not they can regurgitate an epsilon-delta proof.

This isn't a knock on calculus courses, there is an opportunity cost to the time. By the time a continuous math student hits measure theory and understands why they need a(nother) different definition of an integral, most calculus students have been happily chugging along calculating things they need, blissfully ignorant of the "problems" with the integrals they barely remember being defined.

The thing is, you really don't neeed to consider non-Riemann integrable functions if you're actually trying to integrate or measure things. At some point, trying to find non-Borel measurable, but Lebesgue measurable sets serves no practical purpose other than being written down in an analysis textbook. More power to pure mathematicians and their students who enjoy playing these games, but the more applied folks can get around those "problems" by just making some niceness assumptions about your model (like f is Riemann integrable!) and moving on to the more pressing issues in their fields.

Perhaps I was unclear, but we seem to be agreeing.

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

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.

Somewhat famously, symplectic geometry had its fair bit of foundational issues.

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

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

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.

Very interesting project. BTW the Photos link leads to a 404 error and a Hello world.

thanks and thanks for the headsup!

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

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.

But "accelerating development" and "lowering complexity" are, if not synonymous, then at least highly correlated.

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.

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.

Any software dev worth their salt can drop down 1 level in the stack and be productive, if maybe less so. I'd wager most software devs could drop down 2 levels and fully grok everything that is happening.

There is a difference between a Python web developer dropping one level down to examine and debug the SQL the ORM is producing, and dropping one level down to examine and debug a performance problem in the CPython implementation.

In research maths, there are some results you use as a black box because even though you could re-derive the result, it’s just a ton of work and you’re glad someone else has done it. For example perhaps it involves some very tedious case-by-case checking, or a large and long inductive argument. Then there are some results you use as a black box because it would take you (in this case you already have a PhD in the field, so let’s say at least 8 years of field-specific education) literally years of full-time study to become familiar enough with the underpinning technology to even follow the statement of the proof, let alone deeply understand it yourself.

I think there are very few, if any, things in software development that have an analogue in that second category.

> I think there are very few, if any, things in software development that have an analogue in that second category.

Sure, if you're positing that the average developer has a PhD in computer science, or software engineering.

But for the average software developer, gaining an understanding of the implementation details of their preferred programming language, or relational database, or browser HTML rendering engine, etc. (or any of a half dozen or so other systems or components they regularly use as black boxes), would in fact require a similar level of effort.

For any given X, an "X Developer" can mean a developer using X, or a developer of X. The latter is where the analogies lie.

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

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

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.

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.

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

The Lean community uses zulip which seems to be a nice compromise between chat and forum/email threads

https://leanprover.zulipchat.com/login/

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.

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

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"

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…

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.

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

That answer isn't even technically correct unless the man on the ground is in a boat: https://www.google.com/maps/place/42%C2%B000'00.0%22N+60%C2%...

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!

> Why should it be online?

Compare programming before and after Google or before and after StackOverflow.

There is https://mathoverflow.net/

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

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.

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.

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.

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.

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.

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.

Dat uptime tho

Oh snap, I had no idea that he died! Wow... that's a profound loss for the field of mathematics.

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

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.

https://threadreaderapp.com/thread/1419281153983500290.html

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?

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.

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?

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.

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.

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.

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

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

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.

There is no way that AI will be better than us at math in a couple of decades.

Yeah I think I agree now. They'll probably be better at proving straightforward things that don't require any big new insights, but I don't think machines will ever be any good at determining what kinds of new concepts will be interesting to define and explore. Like a machine isn't going to develop calculus just for fun from base principles.

Actually maybe I take that back. I mean, it took how many centuries for humans to invent calculus? Maybe AIs left to their own devices in a reinforcement-learning context could do better.

The interesting thing though, is given free reign to prove whatever they want, they may go off and develop some entirely new field of mathematics and proving really deep stuff, but we just wouldn't recognize it as interesting. Like imagine if such an AI existed 200 years ago and invented Turing machines and proved P != NP, but it wasn't all that great at solving polynomials for whatever reason. We'd have probably thought it was all rubbish and threw it away.

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:

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!

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

> 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?

Some of the famous people just have knack for asking the right questions and then answering them.

I am reminded of a joke that goes something like, if you hit a roadblock in your math problem, the best way to solve it is to get Terry Tao interested in it.

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

I'd draw a distinction between interpreted and compiled languages. It's good to know what an interpreted language does under the hood, and I'd say "look as often as you hit an unexpected performance issue." With compilers, I don't care how the sausage is made... but you'd better believe I'm going over the generated assembly for hotspots.

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?

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.

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

I think they mean computer-verified proofs. As you note, the existing proofs are already formally verified, so this might not add much.

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

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.

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.

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

Lack of gatekeeping and general accessibility of software development is the beauty of this profession.

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.

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.

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!

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)

Behold! http://www.geom.uiuc.edu/~demo5337/Group3/Bhaskara.html

It's so pretty everyone should know it.

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

https://www.reddit.com/r/math/comments/j569y/can_someone_exp...

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

Here is a reply to this tweet thread, posted on behalf of an incarcerated person (christopherhavensmath.com):

"I don't quite agree with much of what is said, but it does also have some truth to it.

The fact is that many people publishing thesis papers are not publishing in major journals and so often have many errors. As well, one can publish a paper that is never refereed by experts in that field at all. Those are disreputable papers. It is our responsibility as mathematicians to pay attention of where the work that we build from comes from. When publishing work, there is a system which ranks the integrity of the academic journals, and my method involves beginning at the best quality journal that is relevant to your work.. the referees attack the paper and send you feedback, possibly rejecting your paper. Then you make adjustments according to their feedback and either resubmit to them, repeating the process, or you submit to the next best journal. After being rejected so many times, your article strengthens more and more until the best possible journal accepts your work.

This method assures that the quality of your work reflects the quality of the publishing journal. My first paper went down the list three notches and landed on a high level journal. But the process of submission was brutal and lasted over two years. There are no gaps in our work (Myself and my 3 coauthors). Rather there are gaps in the understanding of the concepts that immediately surround our work.

When we submit work, often we continue studying in that field and learn rather quickly that our submitted work could have been much better in the sense that you wish you would have included things that are obvious upon countless reviews of your own work. In this sense, good work can have gaps, but that does not necessarily mean that the submission contained errors.

But of course there are many papers out there published through websites or some other means that have zero academic value. The best thing to do is make sure that any research paper you use or reference comes from a reputable journal.

There is one thing to keep in mind... probably the most important part. We research for many reasons. Part of it for me is that research represents the pursuit of beauty. If you're doing math for the reason of adding another notch to your ladder towards academic elitism, then you're doing it for the wrong reason. We are the chasers of mathematical beauty. When we find such beauty the hard part is expressing it flawlessly in the form of human knowledge."

Obligatory pointer to homotopy type theory: https://www.ias.edu/ideas/2014/voevodsky-origins

It's a huge failure of the (mis)education system that almost no one learns math.

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.

Reply on news.ycombinator.com