Yeah, we need a lot more kinds compilers like LEAN. Give the accountants, physicists, chemists, biologists, and so on the tools where they can verify the results.
Every interesting problem I ever had that I checked SO for was either off topic and modded down or the original poster said “I found a solution” and disappeared. Pure misery!
Also, some subset of developers on subscriptions are going to develop products that use the API, and some of those products are going to be successful.
I like the pragmatic take on AI in mathematics. Running off and proving/formalizing things in incomprehensible ways is marginally useful, and probably harmful for any work that needs to move beyond it. But, there's value in what AI is capable of doing for working mathematicians, when used as a partner.
The genie is out of the bottle though. It's hard to see how there won't be weird and inscrutable branches of mathematics that LLMs build and use effectively _for themselves_, in the same way much of the slop LLMs write in spoken language is really for the consumption of LLMs.
Surely there will be a new kind of research mathematician that's investigating this output in the same way, say, academics in literature read.
We research mathematicians are still learning how to use AI in research and how to deal with the output. I drafted eight papers last weekend. This week I advanced on none. AI still gets stuck at the key point on a problem where there isn't already a lot of work done. What falls is where techniques not known to the researcher are available and profitably employed - ai brings them into the fray fast - and someone with experience immediately sees where to go with it - and the dominos fall.
So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.
What's not clear is how the professional infrastructure will survive. Journals seem likely to die. The arxiv is swamped. A human can't assess the volume of the output. Serious conjectures have fallen and serious people have checked them.
We are looking for constructive and productive and socially useful ways forward. One reflection is that a lot of what we have been doing was maybe not so interesting as we thought.
> where techniques not known to the researcher are available and profitably employed - ai brings them into the fray fast - and someone with experience immediately sees where to go with it
> So far AI still doesn't make definitions. It tries but it doesn't really see structure - only patterns on which it can impose (by brute force) known structures.
Insightful and nicely phrased!
Mathematicians are victims of their own success, by systematizing Formalism which made AI possible in the first place.
Paradoxically, they should also be indicted for removing the Human element by deemphasizing the study of Philosophy of Mathematics (i.e. ontology/epistemology/discovery/invention) and its mapping to Reality, but focusing only on formalization as an end in itself.
As you point out, the "definitions" (i.e. conceptual theory) are what is the critical aspect of discovering/inventing/doing mathematics and this has been forgotten in mathematics education since the Formalists gained ascendancy.
I think it is time to go back to the foundations of Mathematics and its Teaching viz. various types of Logical Reasoning, discovered/invented structures and their relationships based on Reality (the ontology and epistemology), with the final goal of understanding Nature itself.
Only a minor in mathematics here. That's interesting that it struggles with definitions. Maybe unsurprising given the different ways they're chosen and written (motivational, aesthetic, pedagogical, etc)? A big lever to keep hold of.
> Any time I tried to use an LLM for a game-y thing, it would fall over. Maybe this is my own bias. I’ve been a game programmer for nearly 15 years, I think I know how things work. I can sniff out “bad” game code a mile away. But when it comes to Svelte web-apps, I’m decidedly less well versed and am inclined to think that whatever code the LLM produces is “good”.
It feels like the discovery of a specific form of gell-mann amnesia. I know when working with an agent through areas where I have domain expertise I catch bad assumptions, decisions, etc. But then, unfortunately, have to trust it much more where I have minimal expertise.
That's a good point. If we don't figure out how to design for what we call consciousness it might be that what emerges from some future neural network is an alien mind that's very different from what humans would call conscious. Could that be called AGI?
That's still very distant from what people are calling AI today.
> very different from what humans would call conscious
I mean, what would you call conscious? The word literally means “aware; responding to one’s surroundings.” By that definition most any animal is conscious and LLM+Harness combos have been conscious for a while.
I think the real issue is that when most people refer to consciousness, they have their own subjective experience in mind which strongly resists any tidy definition. I think it’s extraordinarily unlikely LLMs have anything like this, but they are far more able to effectively respond to their surroundings than most animals and in some areas better than humans.
So if you’re waiting for proof that an LLM has an inner life basically equivalent to your own, you’ll be waiting a long time. After all, other humans can’t even prove the fact of their own consciousness to you! They could just be replaying their training data at you in a way that is merely a convincing but false simulation of the true consciousness which you experience inside your head.
people define consciousness quite differently but it generally has to do with phenomenal experience. your provided definition would make a self-driving car conscious, which is fine to argue, but probably not intended.
I strongly disagree that llm's are conscious of their environment. Even an insect reacts to light and someone attempting to swat at it. An llm barely even receives input from its environment.
By your rules, LLMs & deaf-blind people are not conscious, but self-driving cars are? Also a brain in a vat is not conscious?
The real answer is that we don't know if LLMs are conscious, and we don't really know how we'd that figure out. I guess if an AI wrote a philosophy paper on consciousness that had new insights, that might change some minds. But even that would fail to convince most people.
These are not my rules. I was responding to the person above me. It was he who was saying consciousness is responding to the environment. I too disagree with that definition. A thermometer or a NAND gate responds to its environment but I do not believe either is conscious.
Again, by our own choices and somewhat hardware limitations.
There is nothing stopping you from adding any kind of sensors you want during a training to an LLM, except money and GPU power at this point.
This seems no different to me at least then someone back in the 80's telling me computers were useless because they were so slow. Hardware only gets faster and more efficient from here.
Nope, animals are conscious and yet not AGI, so the two aren't equivalent.
Could consciousness emerge from any system capable of AGI? I doubt it: intelligence is only one axis, and consciousness probably depends on others, like memory, self-reflection (one's output feeding back as input), and continuous operation that reacts to events from both the environment and the self.
I’d argue intelligence is closer to being able to survive and fend for oneself in a dynamic environment than it is making the next scientific breakthrough.
Yeah mind boggling for many here I’m sure.
That’s why the bizarre paradox is llm’s will be better than humans at some complex things but useless at many things that humans regard as being simple. E.g the leap of faith re. LLM’s and robotics.
reply