Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

twitter.com

Post reply on HN
Print view View original

111–120 of 208 posts

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#111

Post by madrox »

bitwize wrote: post #71
madrox wrote: post #66

Earlier quoted context omitted.

> I've always said this but AI will win a fields medal before being able to manage a McDonald's. I love this and have a corollary saying: the last job to be automated will be QA. This wave of technology has triggered more discussion about the types of knowledge work that exist than any other, and I think we will be sharper for it.

The ownership class will be sharper. They will know how to exploit capital and turn it into more capital with vastly increased efficiency. Everybody else will be hosed.

I'm not sure if people will be more hosed than before. Historically, what makes people with capital able to turn things into more capital is its ability to buy someone's time and labor. Knowledge labor is becoming cheaper, easier, and more accessible. That changes the calculus for what is valuable, but not the mechanisms.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#112

Post by slopinthebag »

hodgehog11 wrote: post #86
vatsachak wrote: post #53

Earlier quoted context omitted.

Something like building Linux is more akin to managing a McDonald's than it is to a 10 page technical proof in Algebraic Groups. Programming is more multimodal than math. Something like performance engineering might be free lunch though

> Programming is more multimodal than math I have no idea how you come to this conclusion, when the evidence on the ground for those training models suggests it is precisely the opposite. We are much further along the path of writing code than writing new maths, since the latter often requires some degree of representational fluency of the world we live in to be relevant. For example, proving something about braid gr…

Nah, LLM's are solving unique problems in maths, whereas they're basically just overfitting to the vast amounts of training data with writing code. Every single piece of code AI writes is essentially just a distillation of the vast amounts of code it's seen in it's training - it's not producing anything unique, and it's utility quickly decays as soon as you even move towards the edge of the distribution of it's training data. Even doing stuff as simple as building native desktop UI's causes it massive issues.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#113

Post by Kalabasa »

dunder_cat wrote: post #34
dataviz1000 wrote: post #5

Earlier 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…

> 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…

Nothing as heavy as the above but here's my small anecdote:

I was putting off security updates on my npm dependencies in my personal project because it's a pain to migrate if the upgrade isn't trivial. It's not a critical website, but I run npm scripts locally, and dependabot is telling me things.

I told Claude Code to make a migration plan to upgrade my deps. It updated code for breaking changes (there were API changes, not all fixes are minor version upgrades) and replaced abandoned unmaintained packages with newer ones or built-in Node APIs. It was all done in an hour. I even got unit tests out of it to test for regressions.

In this case, I was able to skip the boring task of maintaining code and applying routine updates and focus on the fun feature stuff.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#114

Post by sealeck »

narrator wrote: post #97
hodgehog11 wrote: post #87

Earlier quoted context omitted.

This argument, that LLMs can develop new crazy strategies using RLVR on math problems (like what happened with Chess), turns out to be false without a serious paradigm shift. Essentially, the search space is far too large, and the model will need help to explore better, probably with human feedback. https://arxiv.org/abs/2504.13837

The search space for the game of Go was also thought to be too large for computers to manage.

Yes and making a horse drawn cart drive itself was thought to be impossible so why don't we have faster than light travel yet...

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#115

Post by in-silico »

ryanar wrote: post #81
vatsachak wrote: post #36

I'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…

Are they actually producing new math? In the most recent ACM issue there was an article about testing AI against a math bench that was privately built by mathematicians, and what they found is that even though AI can solve some problems, it never truly has come up with something novel and new in mathematics, it is just good at drawing connections between existing research and putting a spin on it.

I'm not accusing you in particular, but I feel like there's a lot of circular reasoning around this point. Something like: AI can't discover "new math" -> AI discovers something -> since it was discovered by AI it must not be "new math" -> AI can't discover "new math"

For example, there was a recent post here about GPT-5.4 (and later some other models) solving a FrontierMath open problem: https://news.ycombinator.com/item?id=47497757

That would definitely be considered "new math" if a human did it, but since it was AI people aren't so sure.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#116

Post by in-silico »

TrainedMonkey wrote: post #7
adrithmetiqa wrote: post #2

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.

> generative-AI-is-strictly-limited-to-training-data

Anyone who understands reinforcement learning already knows that's not the case.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#117

Post by abcde666777 »

bitwize wrote: post #98
abcde666777 wrote: post #79

Earlier quoted context omitted.

A bit optimistic I'd say. It's put some software engineering within reach of some people who couldn't do it prior. Where 'some' might be a lot, but still far from all. I was thinking the other day of how things would go if some of my less tech savvy clients tried to vibe code the things I implement for them, and frankly I could only imagine hilarity ensuing. They wouldn't be able to steer it correctly at all and woul…

It's still going to take a knowledgeable person to steer an LLM. The point is that code written entirely by humans is finished as a concept in professional work—if you're writing it yourself you're not working efficiently or employing industry best practice.

I think it's dramatic to say it's the end of hand written code. That's like saying it's the end of bespoke suits. There are scenarios where carefully hand written and reviewed code are still going to have merit - for example the software for safety critical systems such as space shuttles and stations, or core logic within self-driving vehicles.

Basically when every single line needs to be reviewed extremely closely the time taken to write the code is not a bottleneck at all, and if using AI you would actually gain a bottleneck in the time spent removing the excess and superfluous code it produces.

And my intuition is that the line between those two kinds of programming - let's call them careful and careless programming to coin an amusing terminology - I think that line may not shrink as far back as some think, and I think it definitely won't shrink to zero.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#118

Post by jfim »

smokel wrote: post #39
vatsachak wrote: post #36

I'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.

> If your paycheck depended on following the instructions of an AI robot, the world might start to look pretty scary real soon.

That's already the case, minus AI, for gig workers. Their only agency is to accept or decline a ride/delivery, the rest is follow instructions.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#119

Post by zeroonetwothree »

hodgehog11 wrote: post #86
vatsachak wrote: post #53

Earlier quoted context omitted.

Something like building Linux is more akin to managing a McDonald's than it is to a 10 page technical proof in Algebraic Groups. Programming is more multimodal than math. Something like performance engineering might be free lunch though

> Programming is more multimodal than math I have no idea how you come to this conclusion, when the evidence on the ground for those training models suggests it is precisely the opposite. We are much further along the path of writing code than writing new maths, since the latter often requires some degree of representational fluency of the world we live in to be relevant. For example, proving something about braid gr…

I guess the comment you are replying to really meant to say “software engineering” not “programming”.

Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem

#120

Post by zer00eyz »

bitwize wrote: post #71
madrox wrote: post #66

Earlier quoted context omitted.

> I've always said this but AI will win a fields medal before being able to manage a McDonald's. I love this and have a corollary saying: the last job to be automated will be QA. This wave of technology has triggered more discussion about the types of knowledge work that exist than any other, and I think we will be sharper for it.

The ownership class will be sharper. They will know how to exploit capital and turn it into more capital with vastly increased efficiency. Everybody else will be hosed.

There is a fundamental problem with this thinking, you are making an assumption about scale. There is the apocryphal quote "I think there is a world market for maybe five computers".

You have to believe that LLM scaling (down) is impossible or will never happen. I assure you that this is not the case.

Post reply on HN