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.
Mathematics in the age of AI
71–80 of 292 posts
Re: Mathematics in the age of AI
#72Earlier 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…
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
#73Earlier 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?
Re: Mathematics in the age of AI
#74Tao'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…
Re: Mathematics in the age of AI
#75Re: Mathematics in the age of AI
#76Earlier 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.
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
#77Earlier 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…
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
#78Earlier 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?
Re: Mathematics in the age of AI
#79If 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
#80Terence 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…
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.