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

91–100 of 193 posts

Re: AI in mathematics is forcing big questions

#91

Post by _zoltan_ »

mittensc wrote: post #90
hiAndrewQuinn wrote: post #84

Earlier quoted context omitted.

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…

There's a difference in math between giving just the answer to a problem and doing it properly/elegantly. So yeah, generated machine-valid proof can be denied if it's incomprehensible, same as human machine-valid proof can be denied for same reasons.

there is a difference but it's overrated. if a theorem is proven, then, as OP said, the theorem is the interface, no matter where the proof is.

just as we don't re-prove Fermat's little theorem every time I use it in a proof, because well, it's a theorem.

Re: AI in mathematics is forcing big questions

#92

Post by scheme271 »

hilbertseries wrote: post #32
therobots927 wrote: post #23

It’s a well known problem in higher mathematics that even if you’ve solved a problem, often the proofs are incredibly long and complex and require an extensive amount of time spent by peers to review it. It would be great if someone could explain to me how AI improves this situation. Even if AI thinks it’s solved a problem, unless the proof is incredibly efficient and well explained, it will be difficult to verify th…

In 2012 Mochizuki claimed to have proved the abc conjecture by developing a new branch of mathematics. He was a respected mathematician, but the theories he had developed were so complex no one could determine if he was correct. It took six years until two number theorists dissected the proof and found a fatal flaw in it.

Mochizuki and a group of mathematicians still claim that Stix and Scholze didn't actually identify a flaw and his proof was published in a journal (where Mochizuki is the chief editor and the reviewers were people from Mochizuki's instituion). I think most of the math community don't believe his proof although Mochizuki and some others claim it's valid.

Re: AI in mathematics is forcing big questions

#93

Post by x______________ »

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…

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

Why not just fork the original master branch of human science to an ai-enhanced one and see where that brings us?

Re: AI in mathematics is forcing big questions

#94

Post by TheOtherHobbes »

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…

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.

Re: AI in mathematics is forcing big questions

#95

Post by hiAndrewQuinn »

TheOtherHobbes wrote: post #94
hiAndrewQuinn wrote: post #84

Earlier quoted context omitted.

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…

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.

Re: AI in mathematics is forcing big questions

#96

Post by 6510 »

FridgeSeal wrote: post #77
crystal_revenge wrote: post #58

Earlier quoted context omitted.

> 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 kno…

If you’re fine with a future like Warhammer 40k where we all have to be Tech Priests making prayers and performing opaque rituals to get things out of the machine god because we no longer understand things, that’s fine, but that’s not a future the rest of us want.

The problem is that you cant stop it. If there is a wrong way to do something, then someone will do it. Thankfully we understand almost nothing already so it will be easy to adapt - and surrender to the will of the machine.

Re: AI in mathematics is forcing big questions

#97

Post by ben_w »

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 see no reason not to accept the vibe coded blob if Lean says it's kosher except anthropocentrism.

The laws of mathematics exist and their truths hold before they are proven by humans or our machines, so in a very real sense the entire point of proving anything in the first place is anthropocentrism.

That, plus cleaning it up may reveal it contains proofs of other things we also want to know. Imagine if this happened to also contain as a sub-part a proof of all the open Millennium Prize Problems? We don't know until we investigate. (If it was a specific list of things to check from rather than expanding humanity's library, we could just ask an AI to do it for us… but as The Wachowski sisters wrote in their most famous script: "I say your civilization because as soon as we started thinking for you, it really became our civilization").

Re: AI in mathematics is forcing big questions

#98

Post by poetaster »

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…

Well, there is something remarkable in human intelligence. We have yet to find anything like it in the known universe. As for the rest, the wise mathematicians are leaning, sorry, hard to lean. TT and co.

Re: AI in mathematics is forcing big questions

#99

Post by crote »

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.

> 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 circle" is a mere curiosity. Calculating a good-enough approximation is trivial, after all. But wanting an exact answer leads to developing calculus, which leads to most modern physics. Science was able to make a giant leap forwards due to the techniques developed, while the actual answer itself is mostly useless.

Re: AI in mathematics is forcing big questions

#100

Post by freehorse »

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.

New techniques and abstractions is how mathematics expand. Mathematics is about studying structures, proving statements is a part of it but it is not all what mathematics is about. If anything, proofs themselves are a means to an end (understanding). Eg Galois developed some techniques and abstractions to prove that there is no general solution to polynomial equations of degree >=5, but these techniques and abstractions gave rise to whole new mathematical fields.

Mathematics has to be also understood from the perspective of theory building, not just problem solving.

Post reply on HN