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

81–90 of 193 posts

Re: AI in mathematics is forcing big questions

#81

Post by teiferer »

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…

Imagine tomorrow all source code for all software disappears.

Would we still be able to use computers? Of course! They don't need the source code to run.

Would we nevertheless be in big trouble? Oh definitely. We'd need to write all software again, from scratch. Some critical parts we could reverse engineer. Maybe even derive some structures that translate back into source code, but only because a human wrote that source code in the first place.

Hopefully the point is clear: A proof, even if it is correct, that is totally obscure and unintelligable by humans is not very useful for mathematics. It's a black box that doesn't further understanding of the structures and approaches to think about them, and that's what math is all about.Just having a big binary blob of a program doesn't help much if you want to add a feature.

That's also why biology is so hard. There is no source code. It's just millions and millions of years of evolution and things have evolved in weird ways that don't really make it easy to understand them, even though they clearly work.

Re: AI in mathematics is forcing big questions

#82

Post by frabcus »

morpheos137 wrote: post #38

Much can be resolved when it is understood math is discovered not created. AI is a tool. if it makes discovery or proof easier that is still mathematics. A proof stands on its own logic regardless how it is derived. The root concern is how ai may provide uplift for mathematical discovery outside of socially expected channels.

I only did undergraduate level in Maths, and to me there is a key aesthetic element which makes it created. The choice of axioms to use, the choice of with theorems are interesting.

Yes the "truth" (doesn't exist, see Gödels theorem) is discovered in a vast, wild landscape that Mathematicians explore.

But which areas are worth exploring is a critical question. Partly driven by application, partly aesthetic. It's a quest for simple things that are a bit surprising, or that were hard to make the statements so simple.

Re: AI in mathematics is forcing big questions

#83

Post by teiferer »

jdw64 wrote: post #66

Someday, human mathematicians might end up doing proofs for proofs. When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it. In those cases, we usually write tests. But when tests get too big, we end up writing tests for the tests. Eventually, it feels like we're heading into an era of proofs for proofs. For me, this problem usually unfolds like this…

> proofs for proofs.

What does that even mean? Sorry, this is just a nonsensical term.

The issue is not that the proofs could be wrong. It's that humans don't understand them even if they are verifibly correct.

In contrast, with software you don't know if it's correct. That's what you have a test for. Even if you understand it, there could be a bug. And tests could have bugs too, so you can have tests for tests. But proofs that are verified are correct. That's it.

Imagine you have a program that is formally proved to be correct. You don't need a test for it. However you might not understand it. Having a test or not does not change that.

TL;DR: Correctness and understandability are (mostly) independent properties.

Re: AI in mathematics is forcing big questions

#84

Post by hiAndrewQuinn »

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 blob if Lean says it's kosher except anthropocentrism.

Re: AI in mathematics is forcing big questions

#85

Post by jdw64 »

teiferer wrote: post #83
jdw64 wrote: post #66

Someday, human mathematicians might end up doing proofs for proofs. When a codebase gets too large, you eventually can't understand all of it. Even code I wrote myself, I can't fully grasp it. In those cases, we usually write tests. But when tests get too big, we end up writing tests for the tests. Eventually, it feels like we're heading into an era of proofs for proofs. For me, this problem usually unfolds like this…

> proofs for proofs. What does that even mean? Sorry, this is just a nonsensical term. The issue is not that the proofs could be wrong. It's that humans don't understand them even if they are verifibly correct. In contrast, with software you don't know if it's correct. That's what you have a test for. Even if you understand it, there could be a bug. And tests could have bugs too, so you can have tests for tests. But…

[dead]

Re: AI in mathematics is forcing big questions

#86

Post by VBprogrammer »

sdenton4 wrote: post #80
zmgsabst wrote: post #70

Earlier quoted context omitted.

No — people don’t successfully use things they don’t understand every day. They approximately use them with varying degrees of success, but also mistakes, broken inferences, etc. My exact point is that your view reduces our ability to do mathematics to that broken, flawed usage and thereby undermines its utility for logical precision: mathematics is only useful because we cleanly understand it. When you try to use ma…

How many people drive cars without knowing how an engine works? Or make a phone call without knowing how voice compression for a cellular network does it's thing? Or eats food without knowing how it came together from the supply chain?

This feels like a stretch. It would be impossible for someone who didn't know how an engine worked to repair or improve the design of it.

Re: AI in mathematics is forcing big questions

#87

Post by dr_dshiv »

teiferer wrote: post #79
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…

> Here’s one way to think about the difference between coming up with a formal proof and having something other mathematicians can use: Here is a other one: hello_world.c versus hello_world.exe (apologies for windows extensions, just for illustration). One is made by a human for human consumption and extension (though legible by a machine). The source code. One is made by a machine for a machine. Unreadable by a huma…

Binaries are executed by machines but are not yet understandable by machines. (Now that we live in an era where machines can understand, imperfectly, like us)

Re: AI in mathematics is forcing big questions

#88

Post by messe »

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 part of the point of mathematics is human understanding. I think most would be willing to accept the proof. They just wouldn't think it's nearly as useful as one that could be understood.

Re: AI in mathematics is forcing big questions

#90

Post by mittensc »

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…

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.

Post reply on HN