Super interesting but what does this mean for us mere mortals?
My understanding is that, if confirmed, this demonstrates that AI can find novel solutions. This is a strong counterpoint to generative-AI-is-strictly-limited-to-training-data.
[flagged]
Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
31–40 of 208 posts
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#32Earlier quoted context omitted.
I got Claude to self reference and update its own instructions to solve making a typed proxy API of any website. After a week, scores of iterations, it can reverse engineer any website. The first few days I had to be deeply involved with each iteration loop. Domain knowledge is helpful. Each time I saw a problem I would ask Claude to update its instructions so it doesn't happen again. Then less and less. Eventually i…
> I went to the coffeeshop and drank very good coffee listening to music. Then at night I sat and had a beer thinking about T.S. Eliot's 'The Wasteland', the effect of industrialization in England at that time and his views of how ennui affected the aristocracy. Well, for those among us that are not aristocracy already, except for the vanishingly small number of people required to oversee such processes, we’re probab…
Lol,a race to the bottom where too many tech savvy people are left unemployed while a few "privileged" get a decreasing buying power to maintain security of the digital tools that keep the whole digital dependent civilizations afloat?
Sounds like a great starting plot for an interesting story.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#33Earlier quoted context omitted.
In the grand scheme it's good to invent things that replace human labor. It frees up people to do more interesting things. The goal should be to put everyone out of a job.
>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 Software Engineers would assume a certain amount of liability and responsibility for the software they develop. That’s regardless of whether they develop it with LLM tools or something else.
For example, you let your tools write slop that you ship without even looking? And it goes on to wreak havoc? That’s professional malpractice. Bad engineer.
If we do this then Software Engineers become the responsible humans in the loop of so-called “AI” systems.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#34Super interesting but what does this mean for us mere mortals?
I got Claude to self reference and update its own instructions to solve making a typed proxy API of any website. After a week, scores of iterations, it can reverse engineer any website. The first few days I had to be deeply involved with each iteration loop. Domain knowledge is helpful. Each time I saw a problem I would ask Claude to update its instructions so it doesn't happen again. Then less and less. Eventually i…
> Edit: This is going to have huge ramifications for the tech security industry as these systems will be able to break security systems as easily it solved the proof. The sooner the good guys, if there are any left, understand this the better it will be for everybody.
What can the good guys do? Fire up Claude to improve their systems? Unless you have it working fully autonomously to counter-act abuse, I don't see how you can beat the "bad guys". There may be some industries where this is a solved problem (e.g. you can do all the validation server-sided, religiously follow best practices to prevent and mitigate abuse), but a lot of stuff like multiplayer video games will be doomed unless they move to a "you must use a locked down system we control" model. I honestly don't consider it liberating as someone that has various hobby projects, that now in addition to plain old DDoS I'll also have people spin up layer 7 attacks with just their credit card. It almost makes me want to give up instead of pushing forward in a world where the worst of the worst has access to the best of the best.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#35Earlier 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.
In the grand scheme it's good to invent things that replace human labor. It frees up people to do more interesting things. The goal should be to put everyone out of a job.
> The goal should be to put everyone out of a job.
Yeah, but why does it need to take the fun jobs first, like painting, writing poems, coding, making music, ...
I want the AI to cook, do the dishes, take out the trash, etc.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#36I'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 able to think on much larger timescales.
Any professional mathematician will tell you that their arsenal is ~ 10 tricks. If we can codify those tricks as latent vectors it's GG
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#37Super interesting but what does this mean for us mere mortals?
I got Claude to self reference and update its own instructions to solve making a typed proxy API of any website. After a week, scores of iterations, it can reverse engineer any website. The first few days I had to be deeply involved with each iteration loop. Domain knowledge is helpful. Each time I saw a problem I would ask Claude to update its instructions so it doesn't happen again. Then less and less. Eventually i…
This type of slop comment is somehow worse than spam.
>After a week, scores of iterations, it can reverse engineer any website
Cool, let’s see the proof.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#38Super interesting but what does this mean for us mere mortals?
My understanding is that, if confirmed, this demonstrates that AI can find novel solutions. This is a strong counterpoint to generative-AI-is-strictly-limited-to-training-data.
Put in the hands of great mathematicians, pencil and paper proved able to write proofs of open problems.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#39I'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.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#40I'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 StockFish using mechanistic interpretability