Live data from Hacker News

Mathematics in the age of AI

arxiv.org

71–80 of 292 posts

Re: Mathematics in the age of AI

#71
post #55
post #28

Earlier quoted context omitted.

The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen. People will just put up the formally verified result and call it a day, and there's no incentive for them or anyone else to clean things up. We'll end up with incomprehensible math because comprehensibility isn't rewarded. No one is going to get a Fields Medal, or tenure, for digesting someone els…

> The problem with that rule of thumb is that unless there's some status/reward for completing the result, it won't happen. He says it shouldn't be able to published if they can't explain it. Publishing it is the reward.

The thing is, the cost of creating these results, and the expertise needed, is being greatly reduced. So it's possible for people who wouldn't actually care about the results to spoil them by just putting out a formalized proof (for example, to Tao's Palomar site). These people wouldn't care about the prestige; they aren't on a career track where that would matter.

Re: Mathematics in the age of AI

#72
post #56

Earlier quoted context omitted.

I don't understand why people are so fixated on the minds doing the mathematics being made out of meat. It seems obvious that soon, minds made of meat aren't going to be able to keep up. Useful thought, rather than hobbyist thought, seems destined to be the exclusive domain of silicon.

> I don't understand why people are so fixated on the minds doing the mathematics being made out of meat. I don't follow - are you surprised that mathematicians have social rules on how they interact with others? You're definitely welcome to set up a journal that takes whatever types of papers you deem acceptable. It's not like they're preventing the dissemination of information by taking this stance. Personally, I w…

Would you hire a SW engineer that only showcases output from compilers, and can't explain the assembly that it wrote?

Since even the engineers that know what's going on aren't actually reading all of the AI output any more (or, if they are, they're not keeping up with their peer's output), why would you care? I don't think humans should waste time trying to understand their code, it's too slow and costly, and the understanding will be blown away the next time the AI changes it anyways.

Software engineering is becoming pasting in vague-ish descriptions of what you want, and then manually testing that what the AI developed is close enough. It seems like math can go in the same direction too, with useful results that improve our technology getting put into a database for other AIs to consume. Removing humans from the loop can speed things up, especially as AI improves, especially when it reaches a self-improvement loop.

As I keep saying, software is no longer skilled labor. Who knows, math may go in the same direction.

Re: Mathematics in the age of AI

#73
post #48

Earlier quoted context omitted.

I believe this rule of thumb will come to fail. The combination of superhuman mathematical reasoning and synthesis in upcoming AI models plus the rapid build-out of scalable formal verification infrastructure means this exponential in math is going to take off quite explosively, and we've barely seen anything yet. Mathematics is going to decisively move beyond human ability fairly soon (within our lifetimes, if not m…

Maybe that will be true when it's math with practical applications, but most theoretical math isn't like that. If it's not practical and it's not for mathematians to understand, what good is it?

One day it might be for the AI's pleasure, the same way it has heretofore been for ours. Or if you prefer, as a byproduct of its programming to acquire knowledge.

Re: Mathematics in the age of AI

#74
post #35

Tao's Rule of Thumb (which applies very well to software): > My own suggested rule of thumb: if the authors cannot convincingly demonstrate that they are able to give a clear, expert-level talk on their results, one that is correct and properly attributed, then the result should not be published. A proof that no human can properly explain should be viewed as incomplete, even if it has been formally verified.

The counterpoint to this comes from chess. High level engines "prove" certain lines correct (not in the mathematical sense) but those "engine lines" are really hard to explain to humans, even by GMs. They can sort of explain that something is a good line but not why. Engines crush GMs and are considered ground truth even if noone really understands what is happening. Would it be a nightmare if math was the same, not…

If the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?

Re: Mathematics in the age of AI

#75

Earlier quoted context omitted.

If you are free from physical and mental labor, you are in fact, not supplying labor, and are therefore surplus to requirements.

Whose requirements?

The employer's, whose salary affords your subsistence.

Re: Mathematics in the age of AI

#76
post #53

Earlier quoted context omitted.

I can almost see two branches of mathematics developing. One which is human-understandable, the other formally verified. I assume the latter is a strict superset of the former?

I suggest "Catching crumbs from the table" by Ted Chiang. Very short piece published in Nature (2000) and well worth a read. Depicts a scenario where modified humans produce science beyond ordinary scientists' comprehension.

This is a theme in Blindsight by Peter Watts as well.

In that setting, field experts working at the bleeding edge are so advanced that non-experts literally can't understand what they're saying at all. So there's a whole class of specialists, "synthesists", that specialize in gaining approximate understanding of the experts' work for the purpose of communicating it to outsiders—perhaps wrongly, according to the expert at least, but hopefully more productively vs the unmediated version.

Re: Mathematics in the age of AI

#77
post #9

Earlier quoted context omitted.

I wonder what his views on the 4 color problem are. One can explain it as the computer checked a bunch of cases and all maps reduce to one of these cases. It doesn’t take an expert to state this. Properly explain is an enormous grey area. Soon, I think, there will be proofs of results that are verified in Lean that are so long that no one will be able to “properly explain”. I don’t think they should be discarded. Res…

Nowadays the proof of resolution of singularities in characteristic zero is considered something you can teach in an intro algebraic geometry course, though. The concepts have been absorbed and are now much better understood. 4CT is very different because so much of it is exhaustive case analysis; you can understand the high-level ideas of the proof as a bright undergraduate, but you still can’t check the cases by ha…

Abhyankar and others spent years trying to find an easier proof. I’m not an algebraic geometer and I don’t know the state of things now. I was under the impression that on the level of Ideals, Varieties, and Algorithms one can introduce the concept and do some calculations but not present a proof of the theorem.

But the point is that pre-AI it was already the case that famous results were published that very few could understand or digest. I think it is reasonable to expect that we will soon be at a point that Lean says a theorem is correct but no human can or will ever understand the proof.

What if Lean verifies Mochizuki’s proof of the ABC conjecture. Do we disregard it becuase no other mathematician understands the proof?

Re: Mathematics in the age of AI

#78
post #35

Earlier quoted context omitted.

The counterpoint to this comes from chess. High level engines "prove" certain lines correct (not in the mathematical sense) but those "engine lines" are really hard to explain to humans, even by GMs. They can sort of explain that something is a good line but not why. Engines crush GMs and are considered ground truth even if noone really understands what is happening. Would it be a nightmare if math was the same, not…

If the proof is formally verified but impossible to understand how would anyone be able to be sure the formal verification is correct? Complex software is bound to have bugs, no?

The whole point of Lean is that you don't need to understand the entire proof to be sure that it's correct. You only need to understand the definition of the theorem being proven, and you need to trust that the relatively small core of Lean is correct.

Re: Mathematics in the age of AI

#79
What is being made is "what are our core values?" argument. One does not need to be a mathematician to know how poorly this worked for large communities when incentives are misaligned...

If a subset of mathematicians, use AI to condense timelines focusing on goal 6.2 exclusively and make rapid progress and reach a proverbial inflection point — one where value proposition of the using this new normal is too enticing to give up — everyone will ask: "This thing is so awesome. Why should I care about your values?"

Re: Mathematics in the age of AI

#80
post #54

Terence Tao's quote about AI's math proofs is relatable outside of pure math: "the writing very often dwells at length on trivialities while passing briefly through — or even actively obscuring — the most interesting and novel portions of the argument."

>Terence Tao's quote about AI's math proofs is relatable outside of pure math: "the writing very often dwells at length on trivialities while passing briefly through — or even actively obscuring — the most interesting and novel portions of the argument." I noticed a long time ago, that the more people focus on trivialities like typos when arguing against someone online, the more compelling the original argument is. B…

I noticed another thing a long time ago.

Some academic cultures have a tradition of formal debates. They are based on the premise that an educated person should be able to argue convincingly for or against any idea, regardless of whether they believe in it. A natural corollary is that you should not let convincing arguments convince you, as the merits of the argument have little to do with the merits of the idea itself.

LLMs have made the situation worse. People's ability to generate convincing arguments now greatly exceeds their ability to evaluate the value of ideas.

Post reply on HN