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

181–190 of 208 posts

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

#181

Post by [deleted] »

tmoertel wrote: post #161
madrox wrote: post #111

Earlier quoted context omitted.

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.

> Historically, what makes people with capital able to turn things into more capital is its ability to buy someone's time and labor. You forgot to include resources : What makes people with capital able to turn things into more capital is their ability to buy labor and resources . If people with more capital can generate capital faster than people with less capital, then (unless they are constrained, for example, by…

[deleted]

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

#182

Post by madrox »

tmoertel wrote: post #161
madrox wrote: post #111

Earlier quoted context omitted.

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.

> Historically, what makes people with capital able to turn things into more capital is its ability to buy someone's time and labor. You forgot to include resources : What makes people with capital able to turn things into more capital is their ability to buy labor and resources . If people with more capital can generate capital faster than people with less capital, then (unless they are constrained, for example, by…

Fair, though I don’t see how AI is really changing the equation here

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

#183

Post by ineedasername »

hodgehog11 wrote: post #87
vatsachak wrote: post #40

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

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

That linked article says its about RLVR but then goes on to conflate other RL with it, and doesn't address much in the way of the core thinking that was in the paper they were partially responding to that had been published a month earlier[0] which laid out findings and theory reasonably well, including work that runs counter to the main criticism in the article you cited, ie, performance at or above base models only being observed with low K examples.

That said, reachability and novel strategies are somewhat overlapping areas of consideration, and I don't see many ways in which RL in general, as mainly practiced, improves upon models' reachability. And even when it isn't clipping weights it's just too much of a black box approach.

But none of this takes away from the question of raw model capability on novel strategies, only such with respect to RL.

[0] https://arxiv.org/pdf/2506.14245

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

#184

Post by bitwize »

slopinthebag wrote: post #107
bitwize wrote: post #98

Earlier quoted context omitted.

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.

That is akin to saying if you aren't using an IDE you are not working efficiently or employing industry best practice, which is insane when you consider people using Vi often run rings around people using IDEs. AI usage is a useless metric, look at results. Thus far, results and AI usage are uncorrelated.

I keep hearing anecdata that suggest significant to huge productivity increases—"a task that would have taken me weeks now takes hours" is common. There is currently not a whole lot of research that supports that, however:

1) there hasn't been a whole lot of research into AI productivity period;

2) many of the studies that have been done (the 2025 METR study for example) are both methodologically flawed and old, not taking into account the latest frontier models

3) corporate transitions to AI-first/AI-native organizations are nowhere near complete, making companywide productivity gains difficult to assess.

However, it isn't hard to find stories on Hackernews from devs about how much time generative AI has saved them in their work. If the time savings is real, and you refuse to take advantage of it, you are stealing from your employer and need to get with the program.

As for IDEs, if you're working in C# and not using Visual Studio, or Java and not using JetBrains, then no—you are not working as efficiently as you could be.

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

#185

Post by tmoertel »

madrox wrote: post #182
tmoertel wrote: post #161

Earlier quoted context omitted.

> Historically, what makes people with capital able to turn things into more capital is its ability to buy someone's time and labor. You forgot to include resources : What makes people with capital able to turn things into more capital is their ability to buy labor and resources . If people with more capital can generate capital faster than people with less capital, then (unless they are constrained, for example, by…

Fair, though I don’t see how AI is really changing the equation here

AI doesn't change the equation; it makes the equation more brutal for people who don't have capital.

If you don't have capital, the only way to get it is by trading resources or labor for it. Most poor people don't have resources, but they do have the ability to do labor that's valued. But AI is a substitute for labor. And as AI gets better, the value of many kinds of labor will go towards zero.

If it was hard for poor people to escape poverty in the past, it's going to be even harder with AI. Unless we change something about the structure of society to ensure that the benefits of AI are shared with poor people.

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

#186

Post by threethirtytwo »

latentsea wrote: post #169
hodgehog11 wrote: post #138

Earlier quoted context omitted.

I used to be worried, but not so much anymore. It used to be the case that the labs were prioritising replacing human creativity, e.g. generative art, video, writing. However, they are coming to realise that just isn't a profitable approach. The most profitable goal is actually the most human-oriented one: the AI becomes an extraordinarily powerful tool that may be able to one-shot particular tasks. But the design of…

On the contrary the depth and breadth we're becoming able to handle agentically now in software is growing very rapidly, to the point where in the last 3 months the industry has undergone a big transformation and our job functions are fundamentally starting to change. As a software engineer I feel increasingly like AGI will be a real thing within the next few years, and it's going to affect everyone.

I don’t write code anymore. I don’t use ide’s anymore. The agent writes code. My job is to manage ai now.

The paradigm shift has already happened to me and there will be more shifts to come.

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

#187

Post by madrox »

tmoertel wrote: post #185
madrox wrote: post #182

Earlier quoted context omitted.

Fair, though I don’t see how AI is really changing the equation here

AI doesn't change the equation; it makes the equation more brutal for people who don't have capital. If you don't have capital, the only way to get it is by trading resources or labor for it. Most poor people don't have resources, but they do have the ability to do labor that's valued. But AI is a substitute for labor. And as AI gets better, the value of many kinds of labor will go towards zero. If it was hard for po…

Ok, I'm following you. You're saying because labor gets cheaper it will be harder to make a living providing labor. Not disagreeing, but I wonder how much weight to give this argument. History shows a precedent of productivity revolutions changing the workforce, but not eliminating it, and lifting the quality of life of the population overall (though it does also create problems). Mixed bag with the arc bending towards betterment for all. You could argue that this moment is unprecedented in history, but unless the human spirit changes, for better or worse, we will adapt as we always have, rich and poor alike.

If the value of many kinds of labor go towards zero, those benefits also go to the poor. ChatGPT has a free tier. The method of escaping poverty will still be the same. Grow yourself. Provide value to your community.

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

#188

Post by vatsachak »

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…

Grid Diagrams can be specified (hopefully) through algebraic equations.

The way that most math is currently done is that someone provides an extremely specified problem and then one has to answer that extremely specified problem.

The way that programming is currently done is through constructing abstractions and trying to create a specification of the problem.

Of course I'm not saying we're close to creating a silicon Grothendieck (I think that Bourbaki actually reads like a codebase) but I'm saying that we're much closer to constructing algorithms that can solve specified programs as opposed to specifying underspecified problems

Think about the difference in specificity of

Prove Fermat's last theorem vs Build a web browser

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

#189

Post by vatsachak »

hodgehog11 wrote: post #88
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…

As a professional mathematician, I would say that a good proof requires a very good representation of the problem, and then pulling out the tricks. The latter part is easy to get operating using LLMs, they can do it already. It's the former part that still needs humans, and I'm perfectly fine with that.

I guess I'm using Rota's vocabulary where he implicitly uses the word trick to mean representation

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

#190

Post by vatsachak »

gottheUIblues wrote: post #170
vatsachak wrote: post #61

Earlier quoted context omitted.

Exactly. It's what the execs are missing. Also animals thrive in underspecified environments, while AIs like very specific environments. Math is the most specified field there is lol

So specified .. that it can actually prove it can't be completely specified by any single specification

All mathematical statements we care about fall out of the purview of incompleteness
Post reply on HN