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.
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.
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.
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.
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.
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.
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".
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.
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:
I'm a bit of a philistine when it comes to cutting edge CS in this area so I'll leave you to it!
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".
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.
OTOH, there was the Italian school of algebraic geometry, but that was more than one single flaw...
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.
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...)
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.
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.
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.
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.
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.
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.
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.
Also keep in mind that a lot of mathematicians are also older, less tech-savvy. This might change in the next decade or two!
Compare programming before and after Google or before and after StackOverflow.
There is https://mathoverflow.net/
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.
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 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."
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.
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.
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.
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.
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.
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.
The main objection is that most proof-assistants use a different logical foundation than modern mathematics. Modern mathematics is built on ZFC whereas most proof assistants, such as Coq, Isabelle, Agda, etc use different logical foundations, such as the Calculus of Constructions.
Many important results in modern mathematics are not easily stated or proven in systems such as CoC. For example, Brouwer's _Fixed Point Theorem_, 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).
Apparently he now uses Coq in his everyday work.
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.
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 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.
This proof has a seriously low bus factor at the moment :scared:
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.
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.
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?
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.
"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."
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 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.
Conversely, there are many ways to do computer-formalization of mathematics, without every doing anything with HoTT.
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 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."
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())
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.
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)
It's so pretty everyone should know it.
"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."