In math, rigor is vital, but are digitized proofs taking it too far?(quantamagazine.org) |
In math, rigor is vital, but are digitized proofs taking it too far?(quantamagazine.org) |
“The edifice of science is not raised like a dwelling, in which the foundations are first firmly laid and only then one proceeds to construct and to enlarge the rooms,” the great mathematician David Hilbert wrote in 1905 (opens a new tab). Rather, scientists should first find “comfortable spaces to wander around and only subsequently, when signs appear here and there that the loose foundations are not able to sustain the expansion of the rooms, [should they] support and fortify them.”
But sometimes, some of the ugly science gets out of the lab a bit too soon, and it usually doesn't end well. Usually people get their hopes up, and when it doesn't live up to the hype, people get confused.
It really stood out during the covid pandemic. We didn't have time to wait for the long trials we normally expect, waiting could mean thousands of deaths, and we had to make do with uncertainty. That's how we got all sorts of conflicting information and policies that changed all the time. The virus spread by contact, no, it is airborne, masks, no masks, hydroxycholoroquine, no, that's bullshit, etc... that sort of thing. That's the kind of thing that usually don't get publicized outside of scientific papers, but the circumstances made it so that everyone got to see that, including science deniers unfortunately.
Edit: Still, I really enjoyed the LK99 saga (the supposed room temperature superconductor). It was overhyped, and it it came to its expected conclusion (it isn't), however, it sparked widespread interest in semiconductors and plenty of replication attempts.
Most people on HN aren't scientists, even if they fancy themselves as such.
1) while many formalists in his day were stress-testing definitions for unexpected gotcha's; some vocal minority were doing formalization as an eccentric art form.
2) commoditized computers running verification software was not available in his day and age
As long as the weakest link was reliance on human brains faithfully attempting to maintain consistency anyway, then it was more productive and fruitful for the economy to focus on translating observations into the language of mathematics.
Once commoditized hardware and minimalistic verification software becomes available, it makes sense to step back and start a machine readable formalization program to translate or verify the main body of mathematics.
Quoting mathematicians of the caliber like Hilbert in 2026 doesn't mean its great guidance in the face of questions Hilbert was never confronted with: with cheap affordable compute, and an enormously expanded number of mathematicians, perhaps its time to formalize the bulk of mathematics.
And it could happen quickly.
A government can mandate that a certain fraction of student scores is assessed on their formalization tasks. Basically turn the job of formalizing mathematics into homework exercises for students. There are students at all levels, undergraduate, graduate, ... If a result isn't proven yet, turn into a temporary axiom, which goes to the collective TODO list.
In a few years all of mathematics that is regularly touched on in academia could be formalized.
Nation states that enforce this will have a large number of mathematicians capable of formalizing systems into machine readable form, and will benefit tremendously compared to nation states that don't (even if the resulting formalizations were public domain: having a sword available is not the same as having workers experienced in smithing such a sword).
Mathematics is going through a huge, quiet, upheaval. The litmus test will be when, if ever, someone wins a Fields using a proof-assistant in an essential way.
To be clear, there's much more to math than writing down and checking proofs. Some of the most important contributions to math have been simply figuring out the right questions to ask, and also figuring out the useful abstractions. Those are both firmly on the "analog" side of math, and they are every bit as important as writing the proofs. But to say that we have this huge body of rigorous argumentation in math, and then to finally do the work of checking it formally is "taking it too far," is a really bewildering take to me.
No, I don't think formalizing proofs in Lean or other proof systems should dominate the practice of math, and no, I don't think every mathematician should have to write formal proofs. Is that really where we're heading, though? I highly doubt it. The article worries about monoculture. It's a legitimate concern, but probably less of one in math than in many other places, since in my experience math people are pretty independent thinkers, and I don't see that changing any time soon.
Anyway, the conclusion from all this is that the improved ability for mathematicians to rely on automated tools to verify mathematical reasoning would be a great asset. In my opinion the outcomes of that eventuality would be overwhelmingly good.
Whether the world is discrete or analog is still an open problem in science. And it looks as if there is more and more evidence that the world is actually discrete at the quantum level.
(1) Math journals are being flooded with AI slop papers loaded with errors. I can see a time when they will require papers to be accompanied by formal proofs of the results. This will enable much of the slop to be filtered out.
(2) Formalization enables AI to do extensive search while staying grounded.
(3) Formalization of the historical math literature (about 3.5M papers) will allow all those results to become available for training and mining, to a greater extent that if they're just given as plain text input to LLMs.
I think it's great that a lot of work is done using proof assistants, because clearly it's working out for researchers; diversity of research and of methods is a great strength of science. I really can't see how you can "push it too far", pen-and-paper proofs are not going anywhere. And as more researchers write machine-checked proofs, new techniques for automating these proofs are invented (which is what my research is about hehe) which will only make it easier for more researchers to join in.
> Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean.
_Some_ mathematicians are trying to formalize _some_ of mathematics using a proof assistant called Lean. It's not a new development, proof assistants have been used for decades. Lean 4 has definitely been gaining popularity recently compared to others, but other proof assistants are still very popular.
> a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library
The article makes it sound like there is a single, universal "The Lean Library" that everyone is restricted to. I assume it refers to mathlib? But at the end of the day it's just code and everyone is writing their own libraries, and they can make their own decisions.
I'm not a mathematician but that doesn't sound right to me. Most math I did in school is comprised concepts many many layers of abstraction away from its foundations. What did you mean by this?
Total amateur here, but it strikes me that one important difference is that performance matters in software in a way that it doesn’t in mathematics—that is, all proofs are equally valid modulo elegance. That means that abstractions in software are leaky in a way that abstractions in mathematics aren’t.
In other words, in software, the same systems get reused in large part because they’ve been heavily refined, in terms of performance, unexpected corner-case behavior and performance pitfalls, documentation of the above, and general familiarity to and acceptance by the community. In math, if you lay new foundations, build some new abstraction, and prove that it’s at least as powerful to the old one, I’d think that you’d be “done” with replacing it. (Maybe downstream proofs would need some new import statements?)
Is this not the case? Where are people getting stuck that they shouldn’t be?
The value of a proof is not only its conclusion but also the insight that it provides through its method.
The goal of mathematics is not to prove as many theorems as possible but rather to gain an ever deeper understanding of why certain statements are true. The way that something is proved can be more or less useful to advancing that goal.
As an example the elementary proof(s) of the prime number theorem are just about as famous as the original proof. Sometimes the second bite of the cherry is even juicier than the first.
Ultimately, a proof is an argument that something is true. The simpler "more elegant" proof is generally going to be more convincing.
You're assuming that the point of interactive theorem provers is to discover new mathematics. While that's an interesting research area, it seems like the more practical application is verifying proofs one has already discovered through other means.
What LLMs are good at is organizing concepts, filling in detail, and remembering to check corner cases. So their use should help mathematicians to get a better handle on what's terra firma and what's still exploration. Which is great. Proof by it-convinced-other-mathematicians doesn't have a flawless track record. Sometimes major theorems turn out to be wrong or wrong-as-stated. Sometimes they're right, but there's never been a complete or completely correct proof in the literature. The latter case is actually quite common, and formal proof is just what's needed.
How good do you think AI will be at proving new results given that training set?
Math is going to change, and change massively. There's a lot of whistling past the graveyard going on from those who are frightened by this prospect.
Refactoring formalized developments is vastly easier than refactoring software or informal math, since you get verified feedback as to whether the refactoring is correct.
But that is because everyone has to switch to the new system. There are no shortage of experimental OSs that do things in different ways. They fail because of switching costs not because making them is hard.
A machine checked proof is valid if it happens once. You dont need the whole world to switch.
Terence Tao is actively using LEAN and working with the LEAN community to prove leading edge mathematics.
That's fine in math. Math is true or it is not. People who overturn popular conjectures in math get fame, not approbation.
Being able to prove things in something like Lean means that stuff like Mochizuki's work on the abc conjecture could be verified or disproven in spite of its impenetrability. Or, at the very least, it could be tackled piecemeal by legions of students tackling a couple of pages every semester.
It'll keep going on and on.
You've got the wrong idea of what mathematicians do now. There's not a proof shortage! We've had autonomously discovered proofs since at least Automated Mathematician, and we can have more whenever we want them - a basic result in logic is that you can enumerate valid proofs mechanically.
But we don't want them, because most proofs have no value. The work of a mathematician today is to determine what proofs would be interesting to have ("compelling motivations"), and try to prove them.
Proofs tend to get generated upstream of people trying to investigate something concrete about our models.
A computer might be able to autonomously prove that some function might have some property, and this prove is entirely useless when nobody cares about that function!
Imagine if you had an autonomous SaaS generator. You end up with “flipping these pixels from red to blue as a servis” , “adding 14 to numbers as a service”, “writing the word ‘dog’ into a database as a service”.
That is what autonomous proof discovery might end up being. A bunch of things that might be true but not many people around to care.
I do think there’s a loooot of value in the more restricted “testing the truthfulness of an idea with automation as a step 1”, and this is something that is happening a lot already by my understanding.
Isn't that still an unresolved question? Wave-particle duality and all that.
There are things that need to be done by humans to make it meaningful and worthwhile. I’m not saying that automation won’t make us more able to satisfy our intellectual curiosity, but we can’t offload everything and have something of value that we could rightly call ‘mathematics’.
If you believe Wittgenstein then all of math is more and more complicated stories amounting to 1=1. Like a ribbon that we figure out how to tie in ever more beautiful knots. These stories are extremely valuable and useful, because we find equivalents of these knots in nature—but boiled down that is what we do when we do math
Mathematicians will just adopt the tools and use them to get even more math done.
Or more poetically, "if my grandmother had wheels she would have been a bike[1]" is a folk wisdom precisely because it makes so much sense.
The formal definition of "function" is totally different! This is typically a big confusion in Calculus 2 or 3! Today, a function is defined as literally any input→output mapping, and the "rule" by which this mapping is defined is irrelevant. This definition is much worse for basic calculus—most mappings are not continuous or differentiable. But it has benefits for more advanced calculus; the initial application was Fourier series. And it is generally much easier to formalize because it is "canonical" in a certain sense, it doesn't depend on questions like "which exact expressions are allowed".
This is exactly what the article is complaining about. The non-rigorous intuition preferred for basic calculus and the non-rigorous intuition required for more advanced calculus are different. If you formalize, you'll end up with one rigorous definition, which necessarily will have to incorporate a lot of complexity required for advanced calculus but confusing to beginners.
Programming languages are like this too. Compare C and Python. Some things must be written in C, but most things can be more easily written in Python. If the whole development must be one language, the more basic code will suffer. In programming we fix this by developing software as assemblages of different programs written in different languages, but mechanisms for this kind of modularity in formal systems are still under-studied and, today, come with significant untrusted pieces or annoying boilerplate, so this solution isn't yet available.
[1] Later it was discovered that in fact this set isn't analytic, but that wasn't known for a long time.
[2] I am being imprecise; integrating and solving various differential equations often yields functions that are nice but aren't defined by combinations of named functions. The solution at the time was to name these new discovered functions.
Can't you just formalize both definitions and pick the one to work with based on what you want to do? Surely the only obstacle here is the time and effort it takes to write the formalization?
Or, alternatively, just because you've formalized the advanced calculus version doesn't mean you need to use the formalization when teaching basic calculus. The way we've proven something and the way we teach that something don't have to be the same.
Good answer, but not the best example. In many programming languages, the latter is easily written as an expression:
(x - abs(x)) / 2
Taking the absolute of a number generally is not assumed to be in that set, but there is no generally accepted strict definition.
A step ‘up’ from elementary functions are special functions (https://en.wikipedia.org/wiki/Special_functions). Likewise, that is loosely defined.
For example https://en.wikipedia.org/wiki/List_of_eponyms_of_special_fun... mentions lots of polynomials, one of them https://en.wikipedia.org/wiki/Cyclotomic_polynomial, which definitely are elementary according to https://en.wikipedia.org/wiki/Elementary_function.
Wikipedia also contradicts itself in https://en.wikipedia.org/wiki/Closed-form_expression, where it says
“a closed form expression or formula is one that is formed with constants, variables, and a set of functions considered as basic and connected by arithmetic operations (+, −, ×, /, and integer powers) and function composition. Commonly, the basic functions that are allowed in closed forms are nth root, exponential function, logarithm, and trigonometric functions”
and
“For example, if one adds polynomial roots to the basic functions, the functions that have a closed form are called elementary functions”
That would put the goniometric functions in the basic set allowed in elementary functions.
> The problem is more about how it is reported to the public.
From scientific communicators there's a lot of slop and it's getting worse. Even places like Nature and Scientific American are making unacceptable mistakes (a famous one being the quantum machine learning black hole BS that Quanta published)
But I frequently see those HN comments on ArXiv links. That's not a science communication issue. Those are papers. That's researcher to researcher communication. It's open, but not written for the public. People will argue it should be, but then where does researcher to researcher communication happen? You really want that behind closed doors?
There is a certain arrogance that plays a role. Small sample size? There's a good chance it's a paper arguing for the community to study at a larger scale. You're not going to start out by recruiting a million people to figure out if an effect might even exist. Yet I see those papers routinely scoffed at. They're scientifically sound but laughing at them is as big of an error as treating them like absolute truth, just erring in the opposite direction.
People really do not understand how science works and they get extremely upset if you suggest otherwise. As if not understanding something that they haven't spent decades studying implies they're dumb. Scientists don't expect non scientists to understand how science works. There's a reason you're only a junior scientist after getting an entire PhD. You can be smart and not understand tons of stuff. I got a PhD and I'll happily say I'll look like a bumbling idiots even outside my niche, in my own domain! I think we're just got to stop trying to prove how smart we are before we're all dumb as shit. We're just kinda not dumb at some things, and that's perfectly okay. Learning is the interesting part. And it's extra ironic the Less Wrong crowd doesn't take those words to heart because that's what it's all about. We're all wrong. It's not about being right, it's about being less wrong
I think I disagree. There are formal proofs and informal proofs, there are rigorous proofs and less rigorous proofs. Of course, a rigorous proof requires rigor, but that’s close to tautological. What makes a proof is that it convinces other people that the consequent is true. Rigor isn’t a necessary condition for that.
Tbh, elegance is something programmers should strive for too. Elegant code is easier to build upon, easier to read/understand, easier to modify, easier to adapt. For all the same reasons mathematicians want elegance. Though it's true for many domains. People love to throw around the term "first principles" but that's not something you (usually) start at, that's something you derive. And it's usually not very easy to figure out
I used to do a lot of proofs coming all the way from Peano arithmetics, successor operators and first-order tableaux method.
The fact that the domain of study is countable and computable is obvious because humans can’t really study uncountable or uncomputable things. The process of doing anything at all can always be thought of as narrowing down a large space, but this doesn’t provide more insight than the view that it’s building things up.
The reflexive "in mice" comments seem to be bemoaning how science is done.
The problem is not mice experiments on arxiv, the problem is posting those papers for broader dissemenation to the public, with titles suggesting to the public that cancer has been cured, without prominently pointing out that the experiments were not about cancer in humans.
Fair enough. I'm thinking of cases where a good study that isn't turned into PR slop is dismissed because it was done in mice. Which is fine for most people. But not great if we're treating real science that way.
This is science by ignoramus. It isn't how science works, at least not when it works at its best. Someone advocating for censoring science because it might be misread is not on the side of science.
Read about Lisp, the Computational Beauty of Nature, 64k Lisp from https://t3x.org and how all numbers can be composed of counting nested lists all down.
List of a single item:
(cons '1 nil)
[ 1 | nil ]
List of three items:
(cons '1 (cons 2 (cons 3 nil)))
(list '1 '2 '3)
[ 1 | --> [ 2 | -> [ 3 | nil ]
A function is a list, it applies the operation over the rest of the items:
(plus '1 '2 3')
Which is like saying:
(eval '(+ '1 '2 '3))
Eval will just apply the '+' operation to the rest of the list, recursively.
Whis is the the default for every list written in parentheses without the leading ' .
(+ 1 (+ 2 3))
(+ '1 '(+ '2 '3))
How arithmetic is made from 'nothing':
https://t3x.org/lisp64k/numbers.html
Table of contents:
https://t3x.org/lisp64k/toc.html
Logic, too:
In other words, declarative statements relate to objects in the world, but mathematical statements categorize possible declarative statements and do not relate directly to the world.
Ya, so? Even if automation is only going to work well on the well understood stuff, mathematicians can still work on mysteries, they will simply have more time and resources to do so.
No.
>You can
Not right now, right? I don't think current AI automated proofs are smart enough to introduce nontrivial abstractions.
Anyway I think you're missing the point of parent's posts. Math is not proofs. Back then some time ago four color theorem "proof" was very controversial, because it was a computer assisted exhaustive check of every possibility, impossible to verify by a human. It didn't bring any insight.
In general, on some level, proofs like not that important for mathematicians. I mean, for example, Riemann hypothesis or P?=NP proofs would be groundbreaking not because anyone has doubts that P=NP, but because we expect the proofs will be enlightening and will use some novel technique
Note on the other hand that proving standard properties of many computer programs are frequently just tedious and should be automated.
If you've ever worked on a proof for formal verification, then its...work...and the nature of the proof probably (most probably) is not going to be something new and interesting for other people to read about, it is just work that you have to do.
I'm not sure what your threshold for "trivial" is (e.g. would inventing groups from nothing be trivial? Would figuring out what various definitions in condensed mathematics "must be" to establish a correspondence with existing theory be trivial?), but I see LLMs come up with their own reasonable abstractions/interfaces just fine.