5 ms·

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 i

by sxzygz 6mo ago

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 6mo ago
> 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?
- dooglius 6mo ago
  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
  - pas 6mo ago
    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 https://en.wikipedia.org/wiki/Axiom_of_choice#Real_numbers
  - jfarmer 6mo ago
    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-constructive-dedekind-and-cauchy-reals-in-computation https://mathoverflow.net/questions/236483/difference-between...
- enricozb 6mo ago
  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.
- zarzavat 6mo ago
  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 6mo ago
    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
- nitwit005 6mo ago
  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.
perching_aix 6mo ago
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.
fasterik 6mo ago
>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.
- auntienomen 6mo ago
  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 6mo ago
    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 6mo ago
      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.
- 6mo ago
zozbot234 6mo ago
> 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.
bsder 6mo ago
> 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.
bawolff 6mo ago
> 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 6mo ago
Maths doesn't need a litus test, because its not chemistry. You mentioned ideas being ossified and that might be one of them.
sxzygz 6mo ago
[dead]
deterministic 6mo ago
> 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.
nimish 6mo ago
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.

by sxzygz 6mo ago

msteffen 6mo ago

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

dooglius 6mo ago
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
- pas 6mo ago
  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 https://en.wikipedia.org/wiki/Axiom_of_choice#Real_numbers
- jfarmer 6mo ago
  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-constructive-dedekind-and-cauchy-reals-in-computation https://mathoverflow.net/questions/236483/difference-between...
enricozb 6mo ago
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.
zarzavat 6mo ago
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 6mo ago
  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
nitwit005 6mo ago
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.

perching_aix 6mo ago

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.

fasterik 6mo ago

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

auntienomen 6mo ago
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 6mo ago
  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 6mo ago
    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.
6mo ago

zozbot234 6mo ago

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

bsder 6mo ago

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

bawolff 6mo ago

> 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 6mo ago

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

sxzygz 6mo ago

[dead]

deterministic 6mo ago

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

nimish 6mo ago

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.