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

181–190 of 193 posts

Re: AI in mathematics is forcing big questions

#181

Post by YeGoblynQueenne »

hiAndrewQuinn wrote: post #84
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…

Imo, the proved theorem is the API. And that's really all it has to be. If there are other lemmas, etc buried inside that 200k blob that can be factored out and proved and used themselves, so much the better. But denying a machine-valid proof just because it's incomprehensible with what a human being considers a reasonable effort made to unpack it just seems odd to me. I see no reason not to accept the vibe coded blo…

I guess if I project this argument onto software engineering there is no need to write maintainable code; as long as a vibe-coded blob of horror spaghetti "does the job" demanding that the blob is "comprehensible with what a human being considers a reasonable effort" is anthropocentrism.

Have I treated your argument unfairly?

Re: AI in mathematics is forcing big questions

#182

Post by rbanffy »

hiAndrewQuinn wrote: post #95
TheOtherHobbes wrote: post #94

Earlier quoted context omitted.

You can't deny it if it's true, but the point is to find new techniques and abstractions. A proof you can't extrapolate and learn from is just a checkmark, and about as useful.

I don't think that's the point. I think the point is to prove the statement. The techniques and abstractions are a means to an end; making them the point is being seduced by the beauty of the weapon.

> making them the point is being seduced by the beauty of the weapon

The beauty of the weapon IS the point. What it proves is derived from its use.

Re: AI in mathematics is forcing big questions

#183

Post by tripzilch »

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…

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

I'll remind you of the underhanded C contest and the fact that LLMs are widely documented to take such routes.

Re: AI in mathematics is forcing big questions

#184

Post by tripzilch »

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.

But there is. Human cognition is unrivaled.

You're acting as if current-day AI comes even remotely close of surpassing it, lol.

In fact, please show me a useful mathematical proof unintelligible to a human, or even if you would like to "assume" the existence of such, explain how it could be useful to anyone.

Re: AI in mathematics is forcing big questions

#185

Post by tripzilch »

pfdietz wrote: post #157
whattheheckheck wrote: post #65

Earlier quoted context omitted.

You can also pass pytest with assert 1 = 1...

There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without such cheats.

Are you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest?

Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.

Re: AI in mathematics is forcing big questions

#186

Post by pfdietz »

tripzilch wrote: post #185
pfdietz wrote: post #157

Earlier quoted context omitted.

There are also ways to cheat like that in Lean, but they are all easily identifiable. So when people talk about formalization, they mean formalization without such cheats.

Are you sure? If an AI would generate a huge Lean proof/program, wouldn't there be a way to hide such cheats in it? Like as in the underhanded C contest? Because if you give an AI a goal, and cheating at Lean would satisfy that goal, the AI will do it if it can figure it out.

> wouldn't there be a way to hide such cheats in it?

No.

Re: AI in mathematics is forcing big questions

#187

Post by cweld510 »

hiAndrewQuinn wrote: post #95
TheOtherHobbes wrote: post #94

Earlier quoted context omitted.

You can't deny it if it's true, but the point is to find new techniques and abstractions. A proof you can't extrapolate and learn from is just a checkmark, and about as useful.

I don't think that's the point. I think the point is to prove the statement. The techniques and abstractions are a means to an end; making them the point is being seduced by the beauty of the weapon.

Is the point of math really to prove the statement? Arguably interesting, unproven statements are interesting often specifically because they are hard to prove with existing techniques.

Re: AI in mathematics is forcing big questions

#188

Post by lambdacity »

pfdietz wrote: post #163

The big question is: why is government (or society) funding mathematics? What justifies this use of resources? If it's utility, then why doesn't AI deliver utility? Isn't this an argument for AI? One can expand this to various kinds of utility. Is knowing mathematical statements are true useful? In the ability to produce proofs useful? Does being able to prove carry over to other kinds of reasoning? Is producing a ca…

It's R&D. If you've listened to machine learning, it's heavily based around manifolds, statistics, linear algebra, learning theory, etc. All of which were once pure math.

The entire field of cryptography is built up on number theory, a field which famously a major contributor chose because it could never be useful [for war].

Re: AI in mathematics is forcing big questions

#189

Post by pfdietz »

lambdacity wrote: post #188
pfdietz wrote: post #163

The big question is: why is government (or society) funding mathematics? What justifies this use of resources? If it's utility, then why doesn't AI deliver utility? Isn't this an argument for AI? One can expand this to various kinds of utility. Is knowing mathematical statements are true useful? In the ability to produce proofs useful? Does being able to prove carry over to other kinds of reasoning? Is producing a ca…

It's R&D. If you've listened to machine learning, it's heavily based around manifolds, statistics, linear algebra, learning theory, etc. All of which were once pure math. The entire field of cryptography is built up on number theory, a field which famously a major contributor chose because it could never be useful [for war].

Yes, those are utility arguments. So don't we get more utility if AI now spews out lots of new math results?

Re: AI in mathematics is forcing big questions

#190

Post by godelski »

crote wrote: post #99
hiAndrewQuinn wrote: post #95

Earlier quoted context omitted.

I don't think that's the point. I think the point is to prove the statement. The techniques and abstractions are a means to an end; making them the point is being seduced by the beauty of the weapon.

> I think the point is to prove the statement. I couldn't disagree more. A lot of mathematical "problems" are almost entirely pointless. Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map - it is the math that is developed during the solving process that is valuable! An answer to a question like "what is the exact area of a unit ci…

  > Nobody genuinely cares about the moving sofa problem, or about square packing, or about the minimum number of colors needed to draw a map
Wild examples. These are all extremely useful.

I agree that solving problems along the way is incredibly useful too, but there's no math problem that I'm aware of that's utterly useless. Thing is, math is about abstraction and structure. You're developing tools. Those tools can be used for more than one thing. That's why math is often called a language. It's also why mathematicians and physicists end up being so helpful in other fields, because it was (most of them) about understanding the language of complex problem solving. Even code is math (I find it quite odd programmers are against math and elegance as these are directly in line with their goals, but I guess there's always a Dijkstra EWD already calling this out)

Where I fully agree with you is that solving hard problems advances us. TBH, it doesn't matter what it is. Fund NASA and you not only get men to the moon but velcro, GPS, and global wireless communication. Fund particle accelerators and you get the internet. Fund math and, like you said, you get a tool (calculus) which is worth more money than we can even imagine. The thing is that solving hard problems forces the unknown unknowns to become, at least known unknowns.

Post reply on HN