Honestly I am not impressed with Tao treating "ai" as a threat to mathematicians. He might as well say math itself, specifically linear algebra and gradient descent are a threat to mathematicians. Maybe think of something original rather than pander the hype of day?
Can we get a bullshit kill switch where if your company consumes so many dollars for so long it is dissolved. Bullshit is a far bigger threat than imaginary rogue AI.
It depends on what you produce if you make something in demand it may sell itself. For example if you operate oil wells or an ice cream stand. On the other hand if you manufacture bullshit advertising and sales may be key. What I do get about these llm SAS start ups is LLMs instrinsicaly mimic what is in the corpus so if your goal is to compete in an established product pace sure LLMs may be great autopilot but deterministic programs would be even better on the other hand if you are doing something genuinely innovative them you can expect an llm product manager to containmente it with what is already out there or alternatively make unhinged predictions. Llms have poor judgement for what is not already in the corpus.
If we think that machines that recombine and interpolate our prior out are intelligent then yes we have probably peaked as a species. Anyway evolution is not telological. It may surprise HN posters but people were as intelligent if not more so as present thousands of years ago. When a problem is solved is more a question of attention, reward, available knowledge base, etc. intelligence is an adaptation to solve the problems of biological life. It would be hard to argue that solving this cypher would have increased anyone's reproductive fitness that much hence it was unsolved. Unsolved problems are often so less because of intrinsic difficulty but lack of conditions that impell their resolution. It is not at all surprising that llms with the full human knowledge base at their disposal, ample computational resources, and the programmed reward of finding the best completion are solving unsolved problems nobody needed to solve anyway. This however is not intelligence in the human sense. Humans solve problems for biological advantage in a dynamic landscape. Llms solve problems to optimize a completion function in a fixed pre trained one.
The sphere of human comprehensible mathematics is finite. Once everything is solve it is not necessary to advance the field. The recurring error her is to say ai is not the product of human effort but another agent. Ai is human. Ai may well be speeding up human comprehension of math to its limits in which case there is no further need to advance the field and mathematicians might need to get a job. Why is this a bad thing?
There is a shorter proof but since thinking ossified in the 20th century we won't be sociologicaly ready to accept it at this time. Much of math is playing according to arbitrary culturally enforced rules that are not natural in the sense of being minimum logical requirements. Take the axiom of infinity or the axiom of choice for example. Fundamental math need not be based on zfc but that is what we have chosen as our foundation because we elevated continuity, infinity to ontological higher status than distinguishability. In the past similar cultural barriers were present in math for example imaginary numbers are so called because the name originated as derision. It seems unlikely to suggest that math today is not similarly culturally constrained in certain areas and some things we find confounding are more so due to our choice of foundation than their intrinsic nature.
I don't understand what you are trying to say. Which of the following is it, (or is it something else entirely)?
1. There is a much shorter proof that would also be accepted by lean, we just aren't thinking about the problems in the right way so we can't find it.
On one level this is obviously true, Anthropic did not put any effort in to minimising the length of the proof during its development or afterwards.
2. There is a much shorter proof if we took different axioms instead of the ones built into lean.
I find this much harder to believe, unless your new axiom is basically just FLT. Otherwise all reasonable axioms are not too hard to show as equivalent to each other (in terms of what they prove in PA anyway), so such an equivalence proof would be a small portion of the 13 million lines of lean.
Someday. It is has to do with degrees of freedom and information encoding in terms. Stop assuming operations are external but consider them as relational degrees of freedom of a logical statement. Different complexity statements can support different complexity results.
reply