The problem with this ambition is that it turns mathematics into software development. There’s absolutely nothing wrong with this per se, however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software.

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.

▲

msteffen 11 hours ago | parent | next [-]

> what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software.

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?

▲

zarzavat 8 hours ago | parent | next [-]

I know what you're saying but elegance is not simply an aesthetic concern.

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.

	▲	godelski 3 hours ago \| parent [-]
		Exactly. The reason mathematicians and physicists care about elegance is because they care about understanding things. Elegance, like you said, isn't about aesthetics, even though people seem to think they're synonymous. But the elegance is that you've reduced things to simple components. That not only makes it easier for us humans to understand but it means you're closer to the minimal structure. Meaning you know what matters and more importantly, what doesn't. 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

▲

dooglius 11 hours ago | parent | prev | next [-]

Agreed; e.g. if you prove something about the real numbers, the matter of how R is constructed out of your axiomatic system doesn't matter

	▲	jfarmer 8 hours ago \| parent \| next [-]
		The picture isn't quite so clean in the constructive context, which is what many of these proof systems are rooted in, e.g., https://mathoverflow.net/questions/236483/difference-between...
	▲	pas 8 hours ago \| parent \| prev [-]
		there are questions where the abstraction of real numbers becomes leaky, and some axioms (or their lack) poke through. https://en.wikipedia.org/wiki/Axiom_of_choice#Real_numbers

▲

nitwit005 7 hours ago | parent | prev | next [-]

Some proofs have become extremely long, and the raw size has created worries about correctness. It's easy to make a mistake in hundreds of pages.

Ultimately, a proof is an argument that something is true. The simpler "more elegant" proof is generally going to be more convincing.

▲

enricozb 9 hours ago | parent | prev [-]

Proof irrelevance I don't think is accepted in constructivist situations. Those are, however, not that relevant to the recent wave of AI math which uses Lean, whose type system includes classical mathematics.

▲

fasterik 8 hours ago | parent | prev | next [-]

>The litmus test will be when, if ever, someone wins a Fields using a proof-assistant in an essential way.

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.

▲

pfdietz 4 hours ago | parent | next [-]

Of course, once LLMs are really good at that, they can be set loose on the entire historical math literature, all 3.5M papers worth. And then LLMs can be trained on these formalized results (the ones that turn out upon attempted formalization to have been correct.)

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.

▲

auntienomen 7 hours ago | parent | prev [-]

Exactly this. LLMs really aren't built for discovering new mathematics, especially _interesting_ new mathematics. They're built to try the most obvious patterns. When that works, it's pretty much by definition not interesting.

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.

▲

zozbot234 7 hours ago | parent [-]

LLMs and interactive theorem provers are vastly different. There are AI models that come up with workable formal proofs for ITPs but these aren't your usual frontier models, they're specifically trained for this task.

	▲	auntienomen 7 hours ago \| parent [-]
		ITPs are far older than LLMs in general, sure, but that's a pedantic distraction. What everyone is talking about here (both the comments, and the article) are ITPs enriched with LLMs to make the "smart" proof assistants. The LLMs used in ITPs are not vastly different from the usual chatbots and coding assistants. Just a different reinforcement learning problem, no fundamental change in their architecture.

▲

nimish 2 hours ago | parent | prev | next [-]

We already have had that ossified layer thing multiple times in mathematics. Formalisms change. For example, prior to vector calculus writing out multidimensional PDEs was tedious. Vector calculus has serious issues in its own right, so you get people pushing geometric algebra. In more rarefied domains you have things like categories and sheafs replacing the previous "ossified" layer.

It'll keep going on and on.

▲

perching_aix 9 hours ago | parent | prev | next [-]

Haven't science and mathematics always worked like this? Models are built, they ossify, and eventually get replaced when they become limiting. Software just makes that process more explicit. Or at least I don't see how math turning into software development would selectively promote this effect.

▲

zozbot234 7 hours ago | parent | prev | next [-]

> however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer

Refactoring formalized developments is vastly easier than refactoring software or informal math, since you get verified feedback as to whether the refactoring is correct.

▲

bawolff 6 hours ago | parent | prev | next [-]

> That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software.

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.

▲

gerdesj 4 hours ago | parent | prev | next [-]

Maths doesn't need a litus test, because its not chemistry. You mentioned ideas being ossified and that might be one of them.

▲

deterministic 4 hours ago | parent | prev | next [-]

> someone wins a Fields using a proof-assistant in an essential way.

Terence Tao is actively using LEAN and working with the LEAN community to prove leading edge mathematics.

▲

bsder 6 hours ago | parent | prev | next [-]

> certain ideas get ossified.

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.

▲

sxzygz 4 hours ago | parent | prev [-]

[dead]