This sounds like a fully general argument against being alive and having experiences; you could equally well call love a "brain hack". I also care a lot about solving practical problems, but the reason it's important to solve them is because it leads to human flourishing, which includes participating in all these activities you're deriding. Otherwise why are we doing anything at all?
The purpose is paying taxes, interest, rent and various tributes to the full extent of your capabilities and to sacrifice your life for the benefit of your rulers if ordered to.
I've been working for a few years now as a private tutor teaching proof-based math to adults. Maybe this should give me an incentive to join in on some of the cynical replies this has gotten, but that's not actually how I find myself feeling. I love teaching, especially in the one-on-one format, but it really doesn't scale; not everyone can afford a human tutor and there probably aren't nearly enough of them to meet the possible demand.
If a product like this worked well --- and I agree Andrew Ng's involvement seems like a positive sign --- then that would be great! Something I would wonder about from my past experience using LLM's for technical subjects is how to replicate a particular side of the student-teacher relationship. Sometimes a new student of mine will need to be told that they don't actually understand something as well as they think they do, and that they'd be better served by going more slowly than they might have wanted to. This "talking you down gently" conversation is one I'm happy to have (and sometimes it's actually me who's wrong!) but I'd be interested to see whether and how well an LLM run by a company that really wants to retain customers could pull this off.
It's hard to say without an actual product, of course. I'm looking forward to seeing what they come out with.
This was definitely something I saw on HN, but for what it's worth, in my conversations that night with other mathematicians no one brought up Lean proofs or peer review even as a joke. We just copied and pasted the polynomials into a computer algebra system and checked it ourselves and then said "holy shit, I guess the Jacobian conjecture is false". Couldn't have taken more than five minutes after we first saw the tweet.
Right, that's what was so funny about it. Finding a counterexample: an incredible mathematical achievement. Verifying a counterexample: barely even a weeknight homework problem in an undergraduate multivariable course.
I worked as a research mathematician for a while, and I've published peer-reviewed math papers. Reading this tweet put me in the strange position of feeling like defending the way peer review works in my (former) field, which I'm not used to doing. Among other problems it goes too slowly, it pays only the participants who provide the least value, and it was designed for a world that hasn't existed for a long time.
But this tweet paints a somewhat misleading picture of the role peer review plays in practice in modern math research. Reading this tweet could leave you with the impression that when someone proves a new result, no one pays any attention until it's gone through peer review and published in a journal. This just isn't true. ArXiv preprints are much more widely read than the journals' version of articles, and they go up essentially as soon as they're written. Certainly no one's waiting the year-plus it would take to get the article published in a journal! And even before that, mathematicians communicate their results to each other through slightly less formal channels, like blogs, conference talks, and regular human word of mouth.
In short, despite the sclerotic and parasitic nature of the journal system, the way ideas get disseminated in the field in practice is actually a lot closer to the ideal prewar picture he's describing in the tweet. I'm led to understand that this was less true before the Internet, but even by the time I started my PhD in 2009 things had been working the way I just described for quite a while.
I've spent some time working both as a math researcher and as a software engineer, and I think this comment actually underrates the similarity between the two fields as they're actually practiced.
Some math research does involve grabbing a single, fully specified conjecture off the shelf and hunting for a proof of it, and it's true that if you manage to solve a long-standing open problem, other mathematicians will be interested no matter how you did it.
But this isn't all of what they do, probably not even most of what they do. Like in software engineering, it's not always obvious which question would be the most useful one to ask. A lot of mathematical work also goes into what we call "theory-building", where you could say that primary work goes into coming up with definitions rather than theorems. Mathematicians also care a great deal about how something is proved; a lot of them are some of the most aesthetically picky people I've ever met. Words like "ugly", "beautiful", "creative", and "boring" are used to describe both definitions and proofs all the time.
From the outside, it can look like all they're doing is pumping out proofs at any cost. But I promise you that when I talk to mathematicians who don't have any experience building software, they have a similarly narrow view of that field as well! Both fields, from the inside, look a lot more human than you might expect.
I think that your take is quite optimistic. Having published in top tier journals my only experience is that mathematicians care about what other mathematicians worked on and failed to solve. Theory building papers are dime a dozen and don't get published in high tier journals unless they solve a problem.
Math is such that most theories are built after solving a problem and actually don't solve a larger class of problems. Etale Cohomology is an example of a rare exception. Grothendieck was mad that Deligne used adhoc complex analysis techniques to prove Weil. But everyone else was thrilled.
Whereas in CS, a good theory (library) solves a large class of problems. The reason being is that CS tackles general problems while math specific ones. Math on average solves problems that don't lead to solutions to other problems.
To me at least, math is more of a game like chess and coding is more of an art. There are aspects which are a game, like performance engineering but I'm pretty sure that LLMs will become superhuman at that soon
If your complaint is about the type of work that gets you published in a fancy math journal, then I'll happily join you on the barricades. Sure, getting a paper into Annals of Mathematics or whatever is more game than art in the sense I think you mean here.
But "what mathematicians care about" is much, much broader than what gets you published in a fancy journal. Mathematics as a human activity is millennia old, much older than the concept of journals or even universities, and that activity is, to me, very beautiful, worth preserving, and more of an art than a game. The incentive structure of academia for the past few decades has done a pretty bad job at preserving that art form, but that doesn't mean mathematicians as actual human beings don't care about it --- if they didn't, they probably would have chosen a different career.
It seems to me you hooked onto the wrong part of proofs vs software compared to what OP meant.
The difference OP cares about isn’t how much one cares about style. Instead the important difference lies in validation. A proof can be validated as either correct or wrong. That type of hard feedback really helps combat the optimism and desire for shortcuts of modern models.
Now, that still doesn’t help an LLM distinguish between good and bad correct proofs. But it still really helps a lot. On top of that, taste in proofs is a lot more uniform than taste in coding. That helps LLMs be better at judging the quality of a proof, because there’s less disagreement in the wider world.
The standards of proof are different from the fundamental operation of "OK, cool, you solved this problem. Why does this problem matter? Isn't it useless? Senseless? Meaningless?" You have this same question whether or not you're in an a priori discipline (mathematics), scientific fields proper, or engineering. "Absolute certainty" has nothing to do with it. I can assure you, people on the job are not looking for The Absolute Truth when doing their jobs, yet they still can question at a solution by asking: are we solving the right problem?
(Although in general, there's no true difference between "I answered the question correctly, but the question was mapped to this thing we call 'reality' wrong", and "I answered the question incorrectly", because you can (try) adding the constraints that you really wanted targeted in case A, to case B, and boom, suddenly a question/answer pair that was "Answered correctly, but question doesn't map to reality" now becomes, "You answered this question wrong". However, individuals generally tend to have some breakpoint to differentiate between the two).
That's a valuable extra distinction between Mathematics and Software.
In Mathematics there is much more clarity on what question you want to answer. It's much less likely you get an answer to a question, and then realize that the question was useless. Whereas in software its almost guaranteed that your first implementation, correct or otherwise, will solve the wrong problem.
If you're saying that math has a consolidating network effect, sure. There are a lot of people who think similar problems are important. I guarantee you that when math was small, that is not the case, and when coming up with new math, that's not the case, and when coming up with sub problems to tackle large problems, that is not the case.
No, what I'm saying is that I don't agree that taste in mathematics is more uniform than taste in coding! Mathematicians argue about taste all the time. Just as you might look at a piece of code and agree that it compiles and doesn't have any fatal bugs but still think it's badly written, hard to follow, hard to modify, or whatever else, mathematicians judge mathematical work using very similar criteria.
I was trained as a mathematician and worked as a math researcher for a little while (now working as a private tutor), and based on my experience I'd say this description is basically right, with one extra wrinkle.
In order to get a Ph.D., you have to do some sort of original research, so in that sense you're working on "previously unsolved stuff" basically right from the start. But that doesn't entail doing anything all that ground-breaking; most Ph.D. dissertations (very much including mine!) contain work that a more senior researcher in the same subfield could probably have produced without too much difficulty. The software development analogy is a pretty good one: a lot of the point of getting junior researchers to do research is to help train them to one day become senior researchers, and often the work itself is nothing all that special.
Given the trajectory of these LLM proofs, this seems like it's going to have to change pretty soon, and to be honest I'm pretty grateful that I'm not in charge of deciding what that's going to look like, because I don't have any good ideas! I'm actually pretty worried about the future of the field.
Unless, of course, the machine being constructed is the prover (and prompts) that proved the results (or achieved whatever result instead of the human achieving it.)
I'm a mathematician, although not doing research anymore. I can maybe offer a little bit of perspective on why we tend to be a little cooler on the formal techniques, which I think I've said on HN before.
I'm actually prepared to agree wholeheartedly with what you say here: I don't think there'd be any realistic way to produce thousand-page proofs without formalization, and certainly I wouldn't trust such a proof without some way to verify it formally. But I also don't think we really want them all that much!
The ultimate reason I think is that what really lights a fire under most mathematicians is the desire to know why a result is true; the explanation is really the product, much more so than just the yes-or-no answer. For example, I was never a number theorist, but I think most people who are informed enough to have an opinion think that the Riemann Hypothesis is probably true, and I know that they're not actually waiting around to find out. There are lots of papers that get published whose results take the form "If the Riemann Hypothesis is true then [my new theorem]."
The reason they'd still be excited by a proof is the hope, informed by experience with proofs of earlier long-standing open problems, that the proof would involve some exciting new method or perspective that would give us a deeper understanding of number theory. A proof in a formal language that Lean says is true but which no human being has any hope of getting anything from doesn't accomplish that.
A proof written in a formal language can absolutely be illuminating to a human, but you have to pick the correct formal language and ecosystem.
Writing proofs in Agda is like writing programs in a more expressive variant of Haskell. Abelson said that “programs must be written for people to read, and only incidentally for machines to execute”, and by the Curry-Howard isomorphism, proofs can be seen as programs. All the lessons of software engineering can and indeed should be applied to making proofs easier for humans to read.
For a quick example, check out my mechanization of Martin-Löf’s 2006 paper on the axiom of choice:
I certainly didn't mean to dispute that! Formal proofs have a lot in common with code, and of course reading code is illuminating to humans all the time.
I meant to be responding specifically to the case where some future theorem-proving LLM spits out a thousand-page argument which is totally impenetrable but which the proof-checker still agrees is valid. I think it's sometimes surprising to people coming at this from the CS side to hear that most mathematicians wouldn't be too enthusiastic to receive such a proof, and I was just trying to put some color on that reaction.
Ah, I do agree with this perspective. I think we must ensure that any such tools emit proofs that are not only valid but also readable.
On the other hand, humans do also occasionally emit unreadable proofs, and perhaps some troubles could have been avoided if a formal language had been used.
I see axiom of choice, and really LEM, as logic's equivalent to limit points in calculus. No, you can't calculate 0/0, but here's what the answer would be if you could. No, you can't prove the truthiness of this statement, but here's what it would be if you could.
I guess one could work in a brand of math whose axioms make defining and using limits impossible, which, maybe if formalization came before the invention of calculus, would make some 17th-century mathematicians feel more comfortable. Though I imagine it would make progress in physics challenging. I think the same about LEM/AoC. Given that almost every element in the power-set of reals is non-measurable, maybe stuff like Banach-Tarski is actually fundamental in real physics: it can't be predicted or computed, but it can be observed.
I would argue is that some portion of ecosystem should be readable by humans.
In programming engineering we already have this: there is human readable high-level code, and there is assembler and lots of auto-generated code.
In proof system we could have the same: key concepts/theorems should be encoded in human readable form, but no need for human to read through millions of generated lines.
Thanks for the reply. I am also a no-longer-practicing mathematician :)
I completely agree that a machine-generated formal proof is not the same thing as an illuminating human-generated plain-language proof (and in fact I suspect without further guidance they will be quite different, see my other stream of thought comment). However, I do think machine-generated formal proofs would be interesting for a few reasons:
1. Sometimes the obvious thing is not true!
2. I think the existence or non-existence of a machine-generated proof of a mathematical claim is interesting in its own right. E.g. what kinds of claims are easy versus hard for machines to prove?
3. In principle, I would hope they could at least give a starting point for a proper illuminating proof. E.g. the process of refinement and clarification, which is present today even for human proofs, could become more important, and could itself be machine-assisted.
Oh, I hope I didn't come off as talking down to you! As I said in another reply here, the intention behind this comment was pretty narrow --- there's a certain perspective on this stuff that I see pretty often on HN that I think is missing some insight into what makes mathematicians tick, and I may have been letting my reaction to those other people leak into my response to you. Sorry for math-splaining :).
Anyway, yeah, if this scenario does come to pass it will be interesting to see just how impenetrable the resulting formal proofs end up looking and how hard it is to turn them into something that humans can fit in their heads. I can imagine a continuum of possibilities here, with thousands of pages of inscrutable symbol-pushing on one end to beautiful explanations on the other.
> The ultimate reason I think is that what really lights a fire under most mathematicians is the desire to know why a result is true; the explanation is really the product, much more so than just the yes-or-no answer
Of course, but a formal system like Lean doesn't merely spit out a yes-or-now answer, it gives you a fully-fledged proof. Admittedly, it may be harder to read than natural language, but that only means we could benefit from having another tool that translates Lean proofs into natural language.
Ideally we'd be able to get a little of both. A proof of such magnitude should likely come with new definitions that are easy to search for in the code and start to reason about independently. Even without looking at the rest of the proof, I imagine we'd be able to deduce a fair amount of the structure just by understanding the new things that are being defined, what existing theorems are being imported, and connecting the dots.
Your comment reminds me of Tao's comment on the ABC conjecture: usually with a big proof, you progressively get new tools and examples of how they can be applied to other problems. But if it's hundreds of pages of formulas that just spits out an answer at the end, that's not how math usually works. https://galoisrepresentations.org/2017/12/17/the-abc-conject...
If these provers do end up spitting out 1000-page proofs that are all calculation with no net-new concepts, I agree they'll be met with a shrug.
I have always wondered about what could be recovered if the antecedent (i.e. in this case the Riemann hypothesis) does actually turn out to be false. Are the theorems completely useless? Can we still infer some knowledge or use some techniques? Same applies to SETH and fine-grained complexity theory.
It depends. The most likely scenario would be that RH holds except in very specific conditions. Then, any dependent theorems would inherit the same conditions. In many cases, those conditions may not affect the dependent theorem, so they'd still be completely valid. In some cases, those conditions may make the dependent theorem useless, like if RH was "all numbers are even", and your theorem was "all numbers % 2 equal zero, because we know even numbers % 2 are zero and we assume RH", then the exception to RH "except odd numbers" would make your theorem devolve to "all numbers % 2 are zero except the odd ones, because we know even numbers % 2 are zero", which is obviously just a restatement of an existing statement.
In other cases, the new condition affects your theorem but doesn't completely invalidate it. So you can either accept that your theorem is weaker, or find other ways to strengthen it given the new condition.
That's all kind of abstract though. I'm not an expert on RH or what other important math depends on it holding up. That would be interesting to know.
I don't know enough about the RH examples to say what the answer is in that case. I'd be very interested in a perspective from someone who knows more than me!
In general, though, the answer to this question would depend on the specifics of the argument in question. Sometimes you might be able to salvage something; maybe there's some other setting where same methods work, or where some hypothesis analogous to the false one ends up holding, or something like that. But of course from a purely logical perspective, if I prove that P implies Q and P turns out to be false, I've learned nothing about Q.
For the articles on my website, I have a pretty janky workflow where I write a LaTeX document that I compile both to a PDF and (using Pandoc) to HTML, which I render with KaTeX. I've been in the market for a while for something that's less fragile but which can still produce both a PDF and visually appealing HTML output starting from a LaTeX source, and it seems like some of the ideas listed here might be what I want! Thanks for the link. (That said, if anyone has a particular recommendation, I'd love to hear it!)
Incomprehensible proofs are indeed still useful to some extent, and I don't think you'll find many mathematicians who would reject them as an answer to the binary question of whether the result is true.
But when you talk about "getting a lot more done," I want to ask, get a lot more done to what end? Despite what mathematicians sometimes write in their grant applications, resolving most of the big open problems in the field probably won't lead to new technologies or anything. To use the Riemann Hypothesis example again, most number theorists already think it's probably true, and there are a lot of papers being published already which prove things like "if the Generalized Riemann Hypothesis is true, then [my new result]".
No one is really waiting around just for the literal, one-bit answer to the question of whether RH is true; if we got that information and nothing else, I'm sure number theorists would be happy to know, but not a whole lot about the work being done in the field would change. It's not just being "satisfying to the curious"; virtually the entire reason we want a proof is to use the new ideas it would presumably contain to do more mathematics. This is exactly what's happened with the proof of the Poincare Conjecture, the only one of the Millennium Problems that's been resolved so far.
This is what I was lamenting in my comment earlier: the thing you're describing, where we set proof-finding models to work and they spit out verifiable but totally opaque proofs of big open problems in math, very well might happen someday, but it wouldn't actually be all that useful for anything, and it would also mean the end of the only thing about the whole enterprise that the people working in it actually care about.
Yeah, I imagine in those situations, an AI proof that the conjecture is false would probably be more interesting and useful than a proof that it is true.
A proof of the conjecture would essentially just move the situation from "we think there could be counterexamples, but so far we haven't found any" to "there really are no counterexamples anywhere, you can stop looking". The interesting thing here would be the explanation why there can be no counterexamples, which is exactly the thing that the proof wouldn't give you.
On the other hand, a counterproof would either directly present the community with a counterexample - and maybe reveal some interesting class of objects that was overlooked so far - or at least establish that there have to be counterexamples somewhere, which would probably give more motivation to efforts of finding one.
(Generally speaking here. I'm not a mathematician and I can't really say anything about the hypotheses in question)
Yeah, that's definitely right --- an explicit counterexample to the Riemann Hypothesis would be very surprising and interesting, and I think that would be equally true no matter whether it was found by a person or a computer! The situation that would be mostly unhelpful is a certificate that the result is true that communicates nothing about why.
I was an algebraic geometer when I was still doing research in the field, and it was definitely true in that corner of the world. Authors are alphabetical, and you usually cite the paper by listing them all, no "et al"'s. I think I didn't even know there was such a thing as "first author" until I worked in ML.
reply