Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AI in mathematics is forcing big questions

spectrum.ieee.org

Post reply on HN
Print view View original

51–60 of 193 posts

Re: AI in mathematics is forcing big questions

#51

Post by crystal_revenge »

skybrian wrote: post #35

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: > A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs a…

> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob

Anyone who understands type theory and how theorem provers work? It's sort of akin to saying "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!", you know because the compilation would have failed otherwise(this is different than saying the program behaves correctly, but that's precisely the difference between formal proofs and compiled programs).

The entire argument both you and Bessis are implying is that mathematics must be human intelligible. But there's absolutely no reason to assume that every mathematical statement must have a human intelligible representation. There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use.

Just because people who don't want this to be true, and I can understand the motivation, doesn't mean that it isn't still the case.

Re: AI in mathematics is forcing big questions

#52

Post by nok22kon »

mmooss wrote: post #42

There's yet another major issue of the centralization of power and knowledge: > Some worry about the accessibility of AI tools. Traditionally, mathematicians have required little more than intuition, training, and a pen and paper to advance their field. If this slow, deliberative process is no longer valued by society, and particularly by research funders, then mathematics could become an elitist activity, only pract…

always has been

the poor kid always had disadvantages, had to help the family, while the rich kid could focus on the math, and maybe get into a good math place with family help

Re: AI in mathematics is forcing big questions

#53

Post by crystal_revenge »

fiforpg wrote: post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

> but I would like to understand the problem, too

But why should it be the case that this is always possible?

It's entirely reasonable that the set of useful mathematical proofs is a proper superset of human intelligible useful proofs.

In fact, to argue the contrary would imply there is something incredibly remarkable about human cognition.

Re: AI in mathematics is forcing big questions

#54

Post by zmgsabst »

crystal_revenge wrote: post #51
skybrian wrote: post #35

Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: > A clear explanation can be found in Alex Kontorovich’s account of his own learning curve with formalized mathematics. In a nutshell: Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics. It exposes clean APIs a…

> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob Anyone who understands type theory and how theorem provers work? It's sort of akin to saying "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!", you know because the compilation would have failed otherwise(this…

You didn’t answer why merge it into a library focused on humans developing mathematics though.

It remains all of those things, sitting alone in its own repository of 200kLOC; what benefit comes from merging it into mathlib?

> There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use.

This is obviously silly:

Things that aren’t human intelligible aren’t human usable, so the restriction is necessary to have a collection of things humans can utilize.

Re: AI in mathematics is forcing big questions

#55

Post by godelski »

avaer wrote: post #19
jackyinger wrote: post #14

Earlier quoted context omitted.

To bluntly put it in a nutshell, and state the obvious: If you don’t understand the problem you can’t be sure that the computer does.

As a programmer I definitely get annoyed when I see code and I don't understand what it does. But I also definitely don't understand the problem if I can't get the computer to understand it, with tests. In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. With all of these questions in the air, epistemology might be making a comeback.

  > In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof.
But programming is a subset of mathematics. They are both formal languages. I suspect the trustworthiness is more in your comfort level than the ability to verify

Re: AI in mathematics is forcing big questions

#57

Post by zmgsabst »

crystal_revenge wrote: post #53
fiforpg wrote: post #11

The use of computers in mathematics has been somewhat controversial from the very start. There are of course all the computer-assisted proofs (see 4 color theorem), as well as the partially-assisted ones (see Viazovska et al on packing problems in dimensions 8, 24). But even finding a solution numerically, then rigorously verifying its properties can leave a lingering sense of incompleteness, of a gap in understandin…

> but I would like to understand the problem, too But why should it be the case that this is always possible? It's entirely reasonable that the set of useful mathematical proofs is a proper superset of human intelligible useful proofs. In fact, to argue the contrary would imply there is something incredibly remarkable about human cognition.

No, it doesn’t imply that.

Just that the set of proofs a human can interpret and the set of statements a human can understand overlap; conversely, you require that the statements/theorems humans can understand be a larger class than the proofs they can understand.

To me, it’s not obvious which of those should be true:

- can we only understand theorems for which we comprehend their proof?

- or can we understand theorems despite not comprehending the proof structure?

Within the mathematics community, opinions differ. But you’re elevating your perspective on that question into a law, without any evidence.

Re: AI in mathematics is forcing big questions

#58

Post by crystal_revenge »

zmgsabst wrote: post #54
crystal_revenge wrote: post #51

Earlier quoted context omitted.

> Who in their right mind would merge a 200,000-line unaudited vibe-coded blob Anyone who understands type theory and how theorem provers work? It's sort of akin to saying "how do you know that a massive C++ program that compiles to machine code compiled to the correct machine code that will actually run and it's just not a random string of bits!?!?!", you know because the compilation would have failed otherwise(this…

You didn’t answer why merge it into a library focused on humans developing mathematics though. It remains all of those things, sitting alone in its own repository of 200kLOC; what benefit comes from merging it into mathlib? > There is also not reason to assume that if we restrict ourselves to the subset of mathematical statements that are human intelligible that this is of any use. This is obviously silly: Things tha…

> Things that aren’t human intelligible aren’t human usable

This is objectively false, people use things every single day they don't understand. We still have plenty of things about the world we don't understand but still find useful.

You are saying anything we know to be the case, but cannot understand why cannot be used? Can we just stop sleeping because we haven't reasoned why sleep is necessary even though we know it is necessary? I mean we still don't really understand gravity (we know how but not why)

Re: AI in mathematics is forcing big questions

#59

Post by zmgsabst »

godelski wrote: post #55
avaer wrote: post #19

Earlier quoted context omitted.

As a programmer I definitely get annoyed when I see code and I don't understand what it does. But I also definitely don't understand the problem if I can't get the computer to understand it, with tests. In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. With all of these questions in the air, epistemology might be making a comeback.

> In some sense I always considered programming to be more trustworthy than maths arguments without the certainty of a solver proof. But programming is a subset of mathematics. They are both formal languages. I suspect the trustworthiness is more in your comfort level than the ability to verify

That depends on who you ask.

Type theory can also be an independent synthetic foundation atop which you build mathematics.

Re: AI in mathematics is forcing big questions

#60

Post by crystal_revenge »

zmgsabst wrote: post #57
crystal_revenge wrote: post #53

Earlier quoted context omitted.

> but I would like to understand the problem, too But why should it be the case that this is always possible? It's entirely reasonable that the set of useful mathematical proofs is a proper superset of human intelligible useful proofs. In fact, to argue the contrary would imply there is something incredibly remarkable about human cognition.

No, it doesn’t imply that. Just that the set of proofs a human can interpret and the set of statements a human can understand overlap; conversely, you require that the statements/theorems humans can understand be a larger class than the proofs they can understand. To me, it’s not obvious which of those should be true: - can we only understand theorems for which we comprehend their proof? - or can we understand theore…

> understand theorems for which we comprehend

I don't know what your distinction between "understand" and "comprehend" but my point was not about these words, but about being "useful" and being "understandable".

I'm saying there's no relationship between a mathematical statement being useful and it being understandable.

If it is true that "understanding is a prerequisite for usefulness" (where "understanding" means that a statement can be proven in a way that is intelligible to humans) was a property of mathematical expressions, then this fact would certainly be useful (we could exclude any statements that no human understand from the world of useful mathematical expression). But, by that definition, we would need to understand that statement, so you would need to be able to prove that "understanding is a prerequisite for usefulness" in a human intelligible way.

Now what I just wrote is in itself not a proof that we can't know, but proving the above statement would involve expressing the claim in a mathematically verifiable way that was also understandable by humans, which does imply something remarkable about human cognition (something that would be intelligible no less!)

Post reply on HN