Hacker News Reader

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.

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

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 does seem like including a few alternative proofs would greatly aid in understanding.

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

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

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

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.

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.

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!

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.

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.

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

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

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