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

121–130 of 193 posts

Re: AI in mathematics is forcing big questions

#121

Post by captainbland »

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 guess the question becomes about if we are meaningfully capable of doing this kind of verification any better than just adding another layer of automation

Re: AI in mathematics is forcing big questions

#122

Post by guyomes »

Beyond the technical aspects, this new technology also leads to fundamental social changes.

In particular, until now, mathematics were one of the rare sciences were great scientists could emerge from any country with a good education system.

With the raise of strong AI tools, only scientists in rich countries with access to those tools might be able to advance faster on the most difficult problems like the millennium problems.

Mathematics might become like experimental sciences were you need to build expensive machines to make further progress, such as nuclear fusion.

Actually, even now, the strongest models in mathematics are only available to a few engineers and a few mathematicians selected by Openai and Google.

Re: AI in mathematics is forcing big questions

#123

Post by layer8 »

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

I don’t think God has any choice regarding math and logic.

Re: AI in mathematics is forcing big questions

#124

Post by skydhash »

program_whiz wrote: post #112
hiAndrewQuinn wrote: post #110

Earlier quoted context omitted.

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

It’s like the Hilbert’s problem and the birth of computers. Turing’s paper is like 66 pages, but the most valuable output is the Turing machine which can be explained in a few paragraphs.

Re: AI in mathematics is forcing big questions

#125

Post by skydhash »

crystal_revenge wrote: post #58
zmgsabst wrote: post #54

Earlier quoted context omitted.

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

> 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

If you go to the fiction side of things, you’ll get a lot of things that humans would like to do, but can’t right now as we’re blocked by physics laws and our own biology. We have harnessed electricity, why can’t we harness gravity?

Re: AI in mathematics is forcing big questions

#126

Post by utopiah »

I'm not a mathematician but AFAICT AI in mathematics only helped for paradigmatic works, either verification of well explained, and even researched, conjectures. Ideas that have been labelled as potentially interesting, are verifiable, and in a well known area. It is already quite useful... but it is NOT about paradigm change. It's not about revolutionary ideas. It's about being able to slightly more efficiently do more of of the same.

It is precisely NOT about big questions but rather potentially covering and thus cornering away all the "small" questions.

PS: already argued for something similar in recent Ergos related work, see comment history.

Re: AI in mathematics is forcing big questions

#127

Post by crote »

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…

"Dear 13th-century Magical Oracle, It is possible to transmute lead into gold?" "Yes. This pile of giant incomprehensible spaghetti[0] is the irrefutable proof that it is possible."

What did the alchemist truly learn from this interaction? Is the answer in any way helpful for him? Will it lead to him making gold, and the implied endless riches it entails? Why should it bring him him to ask follow-up questions with useful answers like "The technology to do this doesn't exist yet and can't be developed within several lifetimes" and "It'll never be economically profitable to turn lead into gold", instead of blindly being fed piecemeal steps in the impossible task of one medieval guy building a LHC?

Writing true statements is absolutely trivial, anyone can do that. There's an endless amount of true statement which have absolutely no value to humanity whatsoever. Their proof is meaningless without something to give it context. "Substatement 1304 is true" has significantly less value than "here's something I call 'group theory', and it might also be helpful solving open issues in fields X, Y, and Z".

Mathematics is about widening our collective understanding. There will of course be some people out there who'll hear "The answer to life, the universe, and everything is forty-two", think "Neato!", and go on with their day without giving it any further thought - but I'd have a hard time calling them mathematicians.

That doesn't mean it is completely useless, of course. A "prove that no efficient algorithm exists to break this new encryption scheme" would be very helpful indeed. Until you realize it neglected to take quantum computing into account, of course.

[0]: https://home.cern/alice-detects-conversion-lead-gold-lhc/

Re: AI in mathematics is forcing big questions

#128

Post by blks »

utopiah wrote: post #126

I'm not a mathematician but AFAICT AI in mathematics only helped for paradigmatic works, either verification of well explained, and even researched, conjectures. Ideas that have been labelled as potentially interesting, are verifiable, and in a well known area. It is already quite useful... but it is NOT about paradigm change. It's not about revolutionary ideas. It's about being able to slightly more efficiently do m…

In my field that sometimes involves some applied mathematics, it definitely help with busy work, giving raw ideas or writing some chain in latex so I don’t have to spell everything in details myself in the doc

Re: AI in mathematics is forcing big questions

#129

Post by NateEag »

hackermailman wrote: post #17
paulpauper wrote: post #8

It's amazing how much attention this issue has gotten. What is lost in the hype is no AI can tell you if a proof is correct. An AI can produce a convincing looking proof, but it can have a subtle but critical error or make an assumption that is unfounded. Thus, it ultimately comes down to humans. A mathematician has to craft the prompt, and mathematician to interpret/check the results. Also, these programs are very e…

AI can't yet come up with any new ideas to make the inductive leap to solve a math problem. New ideas are what get the accolades and using an old idea just means the original author missed something. We are still at the author missed something stage that AI is doing today. It can definitely be a good research assistant though

Thank you for your comment.

I had assumed that the recent OpenAI solution to an Erdos problem represented original mathematical thought.

I went looking for more details, and found this Scientific American article which provided some nuance I had previously missed, namely that the mathematicians involved don't think genAI created any really new mathematics - just applied what existed in an intelligent, elegant way:

https://archive.is/oNCSO

So, impressive though the result is, perhaps your claim has more grounds than I had thought.

Re: AI in mathematics is forcing big questions

#130

Post by jadar »

utopiah wrote: post #126

I'm not a mathematician but AFAICT AI in mathematics only helped for paradigmatic works, either verification of well explained, and even researched, conjectures. Ideas that have been labelled as potentially interesting, are verifiable, and in a well known area. It is already quite useful... but it is NOT about paradigm change. It's not about revolutionary ideas. It's about being able to slightly more efficiently do m…

Isn’t that somewhat similar to everywhere else AI is being employed? More of the same — just faster? We aren’t getting novel software architecture out of AI, those things are still important, but it does help us rule out bad things (bugs, security vulnerabilities, etc) and help us focus on the important things. In that vein, AI could help mathematicians by ruling things out faster.
Post reply on HN