Comment by a2ff6eeb0

1 day ago

Does it matter? It's going to produce proofs far more intricate than humans can understand, outdoing humans and opening new frontiers.

The age of humans comprehending things is coming to an end: our brains just won't have the capacity to make meaningful contributions to science, math, or technology.

We don’t trillions of dollars in LLM investment to build things mathematicians don’t understand. We already have plenty of those, even from ancient times.

As to your second point, Terry Tao already has an answer [1]: the proof isn’t the contribution, shared understanding is. This issue was already raised back when the four-colour theorem was proved. Machine proving and machine proof checking are useful tools but they don’t mean anything without the interpretative work and the communication necessary to build shared understanding.

[1] https://news.ycombinator.com/item?id=49056620

  • If humans have nothing to contribute then shared understanding is a pointless endeavor. It makes sense now in the "centaur" period where human + AI > AI alone, but when AI mathematicians are both more rigorous and more elegant, then taking the time dumbing down their proofs to a human level of understanding is like requiring that we ensure all our current proofs be understandable by a monkey.

    • > If humans have nothing to contribute then shared understanding is a pointless endeavor.

      I agree, but as a software engineer this gives me pause because I keep trying to insist on coding standards but I’m unable to come up with a compelling reason why it matters. Ostensibly the reason we cared about things like DRY and code quality was so that it would be easy to understand and easy to maintain and easy to make changes to later. But it now seems like a shared understanding of the codebase is less important than ever, and it’s more about shoveling requirements in without breaking any existing functionality.

      Is a well tested slopfest better? That seems to be the conclusion for mathematics, so why not software too?

      6 replies →

    • Where is the value in an unintelligible gibberish proof?

      We already have countless examples of such filling up the arXiv, written by hacks long before LLMs started writing proofs. No one cares about them. You might as well build a box blasting radio static into the void. You could save a lot of electricity that way.

      2 replies →

  • Why not? We build cranes to hoist weights construction workers can't lift. We build electron microscopes to measure things physicists can't see.

    Why is it so hard to imagine we can build tools to think thoughts we can't comprehend?

    If there's commercial value, I think it's inevitable. We don't fund mathematicians because it's cute when they understand a problem, but because their work tends to have applications with commercial value. The value can be captured without understanding the details.

    • Can you give an example of an incomprehensible piece of writing (any writing, never mind a proof) that has commercial value commensurate with the costs involved here?

      36 replies →

  • The idea about the goal of mathematics being shared understanding seems to come at a convenient time.

    Mathematicians have never been known to communicate their ideas very clearly.

    Regardless, even that target llms will likely win - an llm will likely be more efficient at teaching me string theory than a professor in a room with 463 other students.

    The llm is the shared understanding.

    • I don't think "shared knowledge" means "shared knowledge between mathematicians and lay persons" (there is no much point in that, the same way a smartphone technician knows how a smartphone works deep down to the details but there is no big interest for society to have every lay persons being informed about it). I think it means "shared knowledge between mathematicians".

      And at this level, while there are anecdotical exceptions, mathematicians have always been pretty decent (with their conferences, workshops, paper publications, international collaborations, ...).

      So, it does not mean "teaching the subject", it means "creating a human network of people that share the understanding". LLM can be useful at telling a human, but you still need a human. The point of Tao is not that LLM is not good at providing explanations, it is that "providing explanations" is not the contribution to science, "the human network" is. It's like saying "LLM are great cook, they generate tons of food in space", but the point of having cooks is so that people can eat food and not die. Having LLM generating mathematical proofs is as useless as having LLM generating food that no one can access: the point was never to "generate proofs" or "generate food", the point was "creating a shared human understanding" or "eating the food so human can survive".

      3 replies →

The entire point of writing proofs is for advancing human understanding. A giant dump of symbols that passes the lean compiler is meaningless besides human beings understanding it.

  • In the field of pure mathematics this might be true, but it has implications regardless for applied math, engineering, and physics.

  • > The entire point of writing proofs is for advancing human understanding.

    Proofs also enable AIs to direct search and generate knowledge. Verifiability is immensely useful for keeping AI grounded.

    One might imagine AI generating enormous numbers of hypotheses and then trying to prove or disprove them, and then mine that data for new abstractions and heuristics.

    • But what does it mean? The theorems are just symbols in lean. The conjectures humans chose are carefully selected to be the questions that are interesting and relevant to our intuition about the real world.

      Math often doesn't have applications for hundreds of years and that application is only possible because people deeply understand it and how it applies to the real world.

      Generating an endless list of true statements doesn't really do anything, those things are already true regardless of whether someone has written a lean program to model them.

      1 reply →

  • An AI may still be able to apply the results without humans understanding the proof.

  • Sometimes the purpose of the proof is simply to demonstrate that some construct is a safe assumption for other more interesting work-- and could still serve that purpose even if it was entirely a black box.

  • No it isn’t, it’s putting it into the corpus which means another LLM doesn’t have to spend a few billion credits the next time.

  • Is it the AI's fault we can't understand? If the GUT is beyond human comprehension does it matter less? We don't apply this reasoning to other animals or even to less capable humans. Besides, the robots may want to ponder maths for their pleasure.

> The age of humans comprehending things is coming to an end: our brains just won't have the capacity to make meaningful contributions to science, math, or technology.

That sentiment makes me cringe. If you understand how LLMs work, you'd know it'll never be possible without a fundamental change in how these work.

We're also supposed to be reaching that point, somehow, without the LLMs ever being intelligent (in the dictionary definition sense, not the "high reasoning model" marketing sense).

Based on observations, the ones who are fooled by the supposed emergent properties, are just that, fools. Any sufficiently unintelligent agent will perceive transformer based LLM text predictors as possessing high intelligence.

  • Maybe you can enlighten us. In what way aren't LLMs able to make new contributions.

    LLMs in agentic harnesses are Turing complete.

    To my best knowledge, we don't know of any greater computational model that the brain is a part of, that LLMs are not.

    • Obviously actual intelligence has an ineffable essential aspect, just like unicorn farts do.

    • First of all, the argument isn't that LLMs (with I assume some automation) cannot be used in searching a problem space. I'm assuming this is what you're referring to, in terms of contributions?

      That's the part where LLMs are used as tools. Which there are plenty of places where they are useful.

      Also, do you know what turning completeness is? Why are you bringing that up here?

      The crowd that AI psychosis has brought to HN is interesting. But not in the "I'd love to learn more" kind

      5 replies →

"The age of humans comprehending things is coming to an end"

That's something AI companies would really want you to believe.

  • > That's something AI companies would really want you to believe.

    Why would I care what they want me to believe?

    Intuitively it would make sense that you can put math ability on a chart with a value for “general public” “smart high schooler” “smart undergrad” “smart PhD/ professional”. And you could place frontier AI somewhere on that chart over time from GPT 2 to now and see the trend.

    Then you’d have to consider that either you believe there is a fundamental limit that is below peak human mathematician level or there’s not.

    • > Why would I care what they want me to believe?

      How would you not care? Are you a robot?

      They can say random stuff with the goal of increasing their shareholder value. Things they spit out do not have to be true. It is not easy to verify things they say, therefore, everything they say should be taken with a huge grain of salt.

      3 replies →

  • that does not make it not true, nor does it make those companies or their products not dangerous. I like looking at videos of animals that tear other animals apart and eat them; lion cubs are super cute; but that does not mean I want to be thrown into a cage with a model of a lion that has not been programmed to be disinterested when it is sated. AIs appear never sated; humans using or making AI wanting money, even less so. I suspect the AIs will understand the cost long before the humans will, not that anyone making money would care.

You’re prescribing elegance to a stochastic generator trained on the wealth of humanity, including 4chan. Let’s set our expectations a bit.

> It's going to produce proofs far more intricate than humans can understand, outdoing humans and opening new frontiers.

I agree.

> The age of humans comprehending things is coming to an end: our brains just won't have the capacity to make meaningful contributions to science, math, or technology.

I don't know if I see this being true for quite a while, if ever.

  • > It's going to produce proofs far more intricate than humans can understand, outdoing humans and opening new frontiers. > I agree.

    There's an infinite space of possible statements and proofs. The only thing that makes certain proofs significant is that human mathematicians consider them significant; if AI came up with a proof of some statement that no humans could understand then no humans would bother investing further resources in building upon it, for the same reason we don't waste computational resources iterating over the infinite space of true statements in first-order logic.

In limited experimentation: AI will certainly make statements that are extremely intricate and hard to understand, in part because they're overcomplicated and in part because they use a bunch of unnecessary terminology.

This is not to say that a human couldn't understand a streamlined version or that the AI would not be better if it made more streamlined statements to begin with.

(I am not saying that everything mathematical that an AI produces is in any sense trivial.)

>The age of humans comprehending things is coming to an end

I'm sure humans will comprehend some things and not others just as now. They may be smarter than me but the Einsteins and the like already were. It may be that the cutting edge gets pushed by AI more than humans at some point though.

It’s possible, but there’s a difference between vastness and difficulty.

Humans can’t compete with AIs on vastness of material they are familiar with, or the depth of effort they are willing and able to throw at a problem.

But scale isn’t the only aspect of difficult scientific endeavours. There’s also theory. And advancements sometimes come through hard graft of knotting together many things. And sometimes they come through the revelation of a deeper truth, or a new framework, a fundamental insight.

AI might help us reach the next level. But that doesn’t mean we won’t understand anything. It could be we have periods of vast intricacy we cannot follow, punctuated by profound elegance we (or at least experts) relatively easily can. And then the scaffolding we needed to get there falls away.

  • I don't think that's true. Human intelligence is limited, and our brains are inefficient machines.

    The tools we built to replace muscles have mostly obsoleted raw strength for tasks like excavating earth.

    There's no reason to think we can't do the same for brains. And then we'll never need to think for a living again. Some people may want to do it as a commercially insignificant hobby, of course, the way people lift and compete in strongman competitions today.

    We'll have AI taking care of our needs, the way a good mother takes care of their children.

    • >our brains are inefficient machines

      The human brain is exceptionally efficient.

    • A good mother doesn't raise children to be dependent upon her for all their needs.

      For this to actually work in a way that benefits our species, humans will need to become something else/next through their interaction with the technology.

      3 replies →

    • Evidently some already stopped thinking way before the advent of these mythical thinking machines

You could be right, but you're making a lot of assumptions about how complexity, scientific understanding, and explanations scale. One of the features of a good scientific discovery is that it often simplifies and compresses things that were previously a bunch of scattered facts. Also, as AI systems improve they'll get better not only at making scientific discoveries, but also at producing understandable explanations.

Then it's pretty bad that LLMs don't understand anything.

They don't know and can't know. Without an external source of input that corrects them, their output can never be verified.

If and only if that is actually true, then perhaps nothing matters. Until then, calling out shenanigans remains a noble art.

> The age of humans comprehending things is coming to an end: our brains just won't have the capacity to make meaningful contributions to science, math, or technology.

Ask yourself: is that really the world you want to live in? It's a world where people, all people, are sidelined.

I think the happy ending of that path is something like Idiocracy. And the more likely ending is something like "automated capitalist economy without the people, because the people couldn't compete."

>produce proofs far more intricate than humans can understand

Math is not magic, a proof is just a series of applications of a set of rules on some axioms. A mathematician could understand any proof given enough time to study it; the only way for AI to make proofs that a human couldn't understand is by making really, really long proofs.

Why would you want something you don't comprehend? How can you be sure it empowers you?

I think perfect rationality doesn't exist, because it is rational to reject something that you don't understand. So rationality of a given physical system will always be bounded.

It's going to produce proofs far more intricate than humans can understand

The thing is, some number of advanced proofs start out "too intricate for most mathematicians to understand" but many of these get rephrase and reframed until they're accessible to undergraduates. Hopefully, AI math can be guided to do that sort of reframing to increase the level of accessible math as well as extend the border of math.

Let’s not jump the gun. Where they are right now they can somewhat match our abilities. We haven’t even gotten to the point where they can self improve.