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

201–208 of 208 posts

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

#201

Post by nextaccountic »

pks016 wrote: post #55

Interesting but not surprising to me. Once a field expert guides the models, they most likely will reach a solution. The models are good at lazy work for experts. For hard or complicated questions, many a time the models have blind spots.

What if there is no solution?

An expert trying to find a solution for a problem with no solution may sometimes spend decades with no results

Worse yet, proving there is no solution often requires totally different techniques

There's some problems that are currently in a limbo of sorts. We tried to tackle them, were not successful, and currently we don't know if we just need new math to solve them, or if they can't be solved at all

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

#202

Post by pks016 »

nextaccountic wrote: post #201
pks016 wrote: post #55

Interesting but not surprising to me. Once a field expert guides the models, they most likely will reach a solution. The models are good at lazy work for experts. For hard or complicated questions, many a time the models have blind spots.

What if there is no solution? An expert trying to find a solution for a problem with no solution may sometimes spend decades with no results Worse yet, proving there is no solution often requires totally different techniques There's some problems that are currently in a limbo of sorts. We tried to tackle them, were not successful, and currently we don't know if we just need new math to solve them, or if they can't be…

That would be something. Definitely more exciting. But, from I have seen so far, the models are not there yet.

It's a tricky situation for people who might want to work on hard problems like this. Is it worth spending time and money fiddling around the models?

In research, you can't show your progress by showing how many ways you have failed (which I don't like). The universities, grant agency etc. require you to work on solvable problems.

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

#203

Post by renewiltord »

DrewADesign wrote: post #196
renewiltord wrote: post #134

Earlier quoted context omitted.

Sure, but that’s fine. I don’t have any allegiance to other software engineers.

Do you think other people’s sense of ethics should be so transactional towards you? Companies that might sell your data to shitty date brokers have no allegiance to you. Muggers have no allegiance to the people they mug. They’re both executing their professional tasks that benefit the people they have allegience to. They’re contributing to the velocity of money in our society. The data might even be used to market be…

Yes, none of these guys have any allegiance to me. Trying to form a union of muggers with a guy trying to mug me won’t work. You’re welcome to try it if you think it will work for you but I’m not going to.

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

#204

Post by DrewADesign »

renewiltord wrote: post #203
DrewADesign wrote: post #196

Earlier quoted context omitted.

Do you think other people’s sense of ethics should be so transactional towards you? Companies that might sell your data to shitty date brokers have no allegiance to you. Muggers have no allegiance to the people they mug. They’re both executing their professional tasks that benefit the people they have allegience to. They’re contributing to the velocity of money in our society. The data might even be used to market be…

Yes, none of these guys have any allegiance to me. Trying to form a union of muggers with a guy trying to mug me won’t work. You’re welcome to try it if you think it will work for you but I’m not going to.

Copout.

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

#205

Post by DrewADesign »

eproxus wrote: post #139
falcor84 wrote: post #30

Earlier quoted context omitted.

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.

I you think you’ll be paid 3 hours of salary for every 5 minutes of work, I have bad news for you. Most likely your 3 hours will be filled with managing 36 different AI sessions at a time and it will slowly break your brain. At least if we keep doing capitalism the way we are.

Tech industry folks have been so coddled for decades that many think their astonishing intellect has earned them a cushy life rather than being in a field with high labor demand. It’s one reason tech workers are often considered arrogant and out of touch… and that’s why people think they can get paid to lightly orchestrate agents to do their jobs. Oof.

If efficiency gains create an oversupply of tech labor, even the bestie BFF bosses will notice the hoards of more qualified people who will kill for any job that pays more than CVS or Uber— so a lot less than most developers make now. The tech world regularly, shamelessly cuts higher-earning higher-skill workers for cheaper “good enough” replacements. Best of luck.

Even many of the folks that see the writing on the wall have fanciful visions of using their astonishingly capable genius developer brain to maintain or quickly re-achieve some of their high status in the trades. As a union tradesman, I’d find that misconception hilarious if I didn’t feel so bad for them. A lot of folks are going to have a lot of bitter medicine to swallow.

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

#206

Post by DrewADesign »

JV00 wrote: post #178
amelius wrote: post #35

Earlier quoted context omitted.

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

I'm not sure cooking is a good example as it is fun, and also automated in many ways

Depends on the person. When I worked as a chef I’d gladly have had a robot cook for me at home if it was affordable.

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

#207

Post by latentsea »

k33d wrote: post #193
latentsea wrote: post #169

Earlier quoted context omitted.

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.

"to the point where in the last 3 months the industry has undergone a big transformation " Oh... this again.

If you look at those operating at the bleeding edge, it doesn't look anything like yesteryear. It's a real step change. Fully autonomous agentic software engineering is becoming a reality. While still in its infancy, some results are starting to be made public, and it's mind boggling. We're transitioning to a full agent-only workflow in my team at work. The engineering task has shifted from writing code to harness engineering, and essentially building a system that can safely build itself to a high quality given business requirements.

Up until recently I kinda feel like the scepticism was warranted, but after building my own harness that can autonomously produce decent quality software (at least for toy problem scale, granted), and getting hands on with autoresearch via writing a set of skills for it https://github.com/james-s-tayler/lazy-developer, I feel fundamentally different about software engineering than I did until relatively recently.

If you look at the step change from Sonnet 4.5 to Opus 4.5 and what that unlocked, and consider the rumoured Mythos model is apparently not just an incremental improvement, but another step change. Then pair it with infrastructure for operating agents at scale like https://github.com/paperclipai/paperclip and SOTA harnesses like the ones being written about on the blogs of the frontier labs... I mean... you tell me what you think is coming down the pipe?

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

#208

Post by gottheUIblues »

vatsachak wrote: post #190
gottheUIblues wrote: post #170

Earlier quoted context omitted.

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

To the contrary (as summarised by Gemini):

Gödel showed that arithmetic cannot prove everything about itself.

Turing showed that computers cannot predict everything about themselves.

Rice showed that we cannot automatically verify what programs will do.

Chaitin showed that mathematics is full of random, unprovable facts.

Lawvere showed that they are all failing for the exact same structural reason!

These are not fringe issues. They define the absolute boundaries of human and machine intelligence.

Post reply on HN