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

111–120 of 193 posts

Re: AI in mathematics is forcing big questions

#111

Post by hiAndrewQuinn »

x______________ wrote: post #93
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…

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

hell yeah brother let's do it

Re: AI in mathematics is forcing big questions

#112

Post by program_whiz »

hiAndrewQuinn wrote: post #110
crote wrote: post #99

Earlier quoted context omitted.

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

"Mathematics isn't about proving the statement! It's about the collection of substatements which lead to the proof of the statement." "Okay, so what determines what is and is not allowed in the collection?" "Whether the given substatement is true or not, of course." Like this is obviously silly, right. In your view you could have two guys both trying to prove or disprove that the area of the unit circle is 3, and yet…

Isn't the question at hand whether its bad for mathematics if "prove the circle has area 3" devolves into 500 lines of inscrutable lean code, vs just having `pi r^2 == 3`? Sure they both "proved" it true/false, but knowing an answer isn't as useful as knowing why its an answer. Knowing an answer does have some value, its just not as valuable. If I can't work it out myself, I just trust the oracle.

Now if you ask "does the area of unit circle equal 4?", I don't really know, but we can go back to the oracle and ask again (we haven't learned the general pattern).

Also, I'm not sure that assuming this 'area of circle' question was cutting edge math, that the oracle wouldn't say 'yes, to a certain level of tolerance'. Can't count how many times I've seen agent decide a test needs to be loosened or deleted because its an "edge case" or "blocking". If you don't understand the proof you might get back 'yes' for some versions of 'is the area of unit circle 3' (depending on complexity of that ask).

Re: AI in mathematics is forcing big questions

#113

Post by indiv0 »

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…

My instinct is to agree with you. I believe that the drive to a deeper understanding of the problems is what helps us unlock new areas of study, and find opportunities to transfer techniques or bridge otherwise unconnected domains.

But let’s consider a hypothetical: what if an intuitive understanding of the true “boundaries” of mathematics (if such things exist) is beyond the capabilities of a human mind? If there truly is no way to simplify some proofs down from 200,000 line incomprehensible gibberish to something you could teach to a high schooler or undergraduate or even a PhD. Is the proof still worthless? Sure, at the moment, it might be. Finding such a proof and understanding the implications of it are different skills, the latter of which AI almost certainly does not possess at the moment. But there may come a time where the AI can view the bigger picture and make the leaps you described (say, an eka-Calculus from an eka-unit-circle). These leaps may be as unintelligible to us as the proof in OP is.

I guess the question is: assuming that we can’t make the proof beautiful enough to spark deeper human understanding, do we still want it if it sparks deeper AI understanding?

Personally I would hate to live in a universe where the boundaries of science are beyond intuitive human understanding, but I think it’s almost certainly the case. The idea that the rules are all within our grasp reeks of anthropocentrism to me. I would love for the universe to prove me wrong though. It’d be a pleasant, hilarious coincidence if they do fit within the boundaries of our understanding.

Re: AI in mathematics is forcing big questions

#114

Post by strogonoff »

stringfood wrote: post #56
rirze wrote: post #41

I think we’re going to find out the hard way that the proofs left to solve are very much not elegant.

couldn't God have created a more orderly universe for us? this is ridiculous

To assume that the universe is disorderly presumes knowing some esoteric objective truth about how the universe works. Since the field of natural sciences does not provide that truth (by design), and practices that do aim to provide that truth (metaphysics, religion, etc.) seem to have different versions of it, I would say that there’s a fair chance that the universe is not that disorderly and we just lack better models for describing it.

Re: AI in mathematics is forcing big questions

#115

Post by bananaflag »

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…

Thank you for spelling this in detail!

One thing I might add is that not all programs can be proved to be correct for the simple reason that not all purposes of a program can be mathematically specified. For example, for (even "closed world" domain programs like) a chess engine, the one thing that matters (in the absence of a complete solution of a game like there exists in checkers) is "can beat world champions", which can only be tested empirically. Or sometimes, e.g. business logic software, the purpose can be mathematically specified but not in a simpler way than the code itself.

Re: AI in mathematics is forcing big questions

#116

Post by AaronAPU »

jstanley wrote: post #61
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…

This is what Lean is for: https://lean-lang.org/ If you have the LLM generate Lean code, and it compiles, then the proof is correct and you don't need to bother checking its working. (You still need to check that it is proving the theorem you asked it to prove).

I’m playing devil’s advocate here, so go easy on me. But how completely do we know lean is perfectly true in all cases?

Re: AI in mathematics is forcing big questions

#117

Post by OtherShrezzing »

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.

Most of the interesting research I’ve ever done started while reading through the intermediate steps in an unrelated paper.

As far as I can tell from colleagues in other domains, it’s the same there. One paper will mention something off-hand and that’ll cause someone else to have a spark of insight, which turns into it’s own valuable research

Re: AI in mathematics is forcing big questions

#118

Post by Diogenesian »

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…

These proof checkers all have bugs, every single one, and since AI is still 100% incapable of understanding simple mathematics we should assume agents are likely to cheat by exploiting a kernel bug. So a human really does have to be able to read and understand the proof. There's no difference between blindly trusting Lean and blindly trusting Grigori Perelman: yes you can be reasonably confident the proof is correct. But you gotta check.

This future of "the AI built the compiler and it's totally incomprehensible spaghetti, but don't worry, it verified the compiler works using this AI-generated proof assistant whose codebase is also pure spaghetti" terrifies me.

Re: AI in mathematics is forcing big questions

#119

Post by practal »

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…

I think 6) is a very good point. The simple reaction to it is, well, I just define a small verification kernel that I trust, and the rest is just scaffolding that does not need to be trusted in order to have full confidence in the verification. Of course, that is not really true, because how do you know that the data arrives properly at the kernel, and is properly read off the kernel? In practice though, the small verification kernel idea works very well. I don't think that this is the final stage of how these systems are designed, though. I think we need to model the full system inside the system, and verify it this way. We can trust this verification because we are verifying it with a system with a small verification kernel, but afterwards, we can replace the small kernel with the modules we have proven to be correct now.

Re: AI in mathematics is forcing big questions

#120

Post by alberto-m »

hiAndrewQuinn wrote: post #110
crote wrote: post #99

Earlier quoted context omitted.

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

"Mathematics isn't about proving the statement! It's about the collection of substatements which lead to the proof of the statement." "Okay, so what determines what is and is not allowed in the collection?" "Whether the given substatement is true or not, of course." Like this is obviously silly, right. In your view you could have two guys both trying to prove or disprove that the area of the unit circle is 3, and yet…

The argument of your imaginary dialogue is very weak. To run a valid marathon one must cover 42 kms, but we do not run marathons because we want to be 42 kms away. Building a robot to do that would be probably an interesting feat for robotics, but it would not leave any mark in the history of the sport.
Post reply on HN