out of curiosity, i wonder if people are taking stabs at p!=np
[deleted]
Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
41–50 of 208 posts
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#42Earlier quoted context omitted.
>It frees up people to do more interesting things Like beg on the corners and starve in the street? Trying to figure out how the basics of capitalism where labor is exchanged for money is not going to work well when the only jobs left are side gigs. Something will have to change and a lot of People will fight said change.
I’ve thought about this myself. Couple of points: 1) It’s not my job to fix all the problems of Capitalism. It’s painful to try to fight the system without collective action. My family and I have to eat too. 2) We have had a solution all along for the particular problem of AI putting devs out of work. It’s called professional licensure, and you can see it in action in engineering and medical fields. Professional Soft…
It’s not your job to fix capitalism. But it is your job to evaluate if your money making skill comes at too high a price for others.
Say you found a job shooting people in the head for money. Like if you work for ICE or something…
You need to feed your family. Is this job ok? You may decide yes. I decided no. I will find another way to feed my family.
You don’t get to escape consequences because you are a small cog in a large system.
In the bigger picture, automation should free people from labor. But that requires some very greedy people to relax their grip ever so slightly. I imagine they see automation as a way to reduce reliance on labor, and if they don’t need labor, they don’t need people. So let them starve and stop having kids.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#43I've always said this but AI will win a fields medal before being able to manage a McDonald's. Math seems difficult to us because it's like using a hammer (the brain) to twist in a screw (math). LLMs are discovering a lot of new math because they are great at low depth high breadth situations. I predict that in the future people will ditch LLMs in favor of AlphaGo style RL done on Lean syntax trees. These should be a…
I think this is mostly about existing legislature, not about technology. In any other context than when your paycheck depends on it, you would probably not be following orders from a random manager. If your paycheck depended on following the instructions of an AI robot, the world might start to look pretty scary real soon.
There's a lot to being a manager
- Coherent customer interaction
- Common sense judgements
- Scheduling
- Quality control
All which are baked into humans but not so much into LLMs
Even if it were legal to have an LLM as a GM, I think it would fair poorly
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#44Earlier quoted context omitted.
I kind of feel like software engineers working on improving AI are traitors working against other SE’s trying to make a living. However… I have to acknowledge my craft of SE has been putting people out of work for decades. I myself came up with business process improvement that directly let the company release about 20 people. I did this twice. So… fair play.
Aren't the true traitors still the ones paying the SE to do that work? The managerial slave-master class?
You always have a choice to make. You make it everyday. Get up. Go to a legitimate job. Work.
You probably choose not to steal, rob, impersonate someone else, or generally make money illegally.
It can be traitors all the way down.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#45I've always said this but AI will win a fields medal before being able to manage a McDonald's. Math seems difficult to us because it's like using a hammer (the brain) to twist in a screw (math). LLMs are discovering a lot of new math because they are great at low depth high breadth situations. I predict that in the future people will ditch LLMs in favor of AlphaGo style RL done on Lean syntax trees. These should be a…
Tricks are nothing but patterns in the logical formulae we reduce. Ergo these are latent vectors in our brain. We use analogies like geometry in order to use Algebraic Geometry to solve problems in Number Theory. An AI trained on Lean Syntax trees might develop it's own weird versions of intuition that might actually properly contain ours. If this sounds far fetched, look at Chess. I wonder if anyone has dug into Sto…
Stockfish's power comes from mostly search, and the ML techniques it uses are mainly about better search, i.e. pruning branches more efficiently.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#46I've always said this but AI will win a fields medal before being able to manage a McDonald's. Math seems difficult to us because it's like using a hammer (the brain) to twist in a screw (math). LLMs are discovering a lot of new math because they are great at low depth high breadth situations. I predict that in the future people will ditch LLMs in favor of AlphaGo style RL done on Lean syntax trees. These should be a…
> AI will win a fields medal before being able to manage a McDonald's
Of course, because it takes multi-modal intelligence to manage a McDonalds. I.e. it requires human intelligence.
> I predict that in the future people will ditch LLMs in favor of AlphaGo style RL
Same for coding as well. LLM's might be the interface we use with other forms of AI though.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#47I've always said this but AI will win a fields medal before being able to manage a McDonald's. Math seems difficult to us because it's like using a hammer (the brain) to twist in a screw (math). LLMs are discovering a lot of new math because they are great at low depth high breadth situations. I predict that in the future people will ditch LLMs in favor of AlphaGo style RL done on Lean syntax trees. These should be a…
I've never seen you say that
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#48Earlier quoted context omitted.
> I would go for a 2 or 3 hour walk with my phone using the remote control feature looking every 5 - 10 minutes to make sure it doesn't need human help. That is a nightmarish scenario tbh
Nightmarish?! In comparison to the average person's actual job? I'm pretty sure that many people out there would sign up for a battle royale for a chance at such a job.
Would they? I'd love to get in touch
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#49Earlier quoted context omitted.
Tricks are nothing but patterns in the logical formulae we reduce. Ergo these are latent vectors in our brain. We use analogies like geometry in order to use Algebraic Geometry to solve problems in Number Theory. An AI trained on Lean Syntax trees might develop it's own weird versions of intuition that might actually properly contain ours. If this sounds far fetched, look at Chess. I wonder if anyone has dug into Sto…
Stockfish's power comes from mostly search, and the ML techniques it uses are mainly about better search, i.e. pruning branches more efficiently.
The weights must still have some understanding of the chess board. Though there is always the chance that it makes no sense to us
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#50I've always said this but AI will win a fields medal before being able to manage a McDonald's. Math seems difficult to us because it's like using a hammer (the brain) to twist in a screw (math). LLMs are discovering a lot of new math because they are great at low depth high breadth situations. I predict that in the future people will ditch LLMs in favor of AlphaGo style RL done on Lean syntax trees. These should be a…
I've never seen you say that
You will have to take my word that I started saying this in Dec 2024 lol