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

141–150 of 208 posts

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

#141

Post by Bombthecat »

specvsimpl wrote: post #124
parineum wrote: post #122

Earlier quoted context omitted.

There is a kind of rubrik I use on stuff like this. If LLMs are discovering new math, why have I only read one or two articles where it's happening? Wouldn't it be happening with regularity? The most obvious example of this thinking is, if LLMs are replacing developers, why us open ai still hiring?

I can only say that at family meetings, I hear people talk about contracting with a shop that used to have 4 web designers, but now it's 1 guy, delivering 4x faster than before. So devs are being replaced.

Nah AI is not replacing people! /s

And other stories people tell themselves to sleep better at night

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

#142

Post by [deleted] »

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

[deleted]

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

#143

Post by throwaway27448 »

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

I agree that LLMs are a bad fit for mathematical reasoning, but it's very hard for me to buy that humans are a better fit than a computational approach. Search will always beat our intuition.

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

#145

Post by Imanari »

qnleigh wrote: post #130

In the paper, they give part of their system prompt: > * After EVERY exploreXX.py run, IMMEDIATELY update this file [plan.md] before doing anything else. * No exceptions. Do not start the next exploration until the previous one is documented here. Is this known to improve performance for advanced problem solving? If so, why this specific prompt?

Maybe to be better able to restart the process and not lose track.

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

#148

Post by abcde666777 »

specvsimpl wrote: post #126
abcde666777 wrote: post #117

Earlier quoted context omitted.

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

You are aware of software verification? The AI can prove (mathematically) that its code implements the spec.

That just takes you back to the debate about the code being the spec.

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

#149

Post by Yoric »

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

This is certainly my hope.

In my spare time, I'm slowly, very slowly, inching towards a prototype of something that could work like that.

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

#150

Post by Eufrat »

dataviz1000 wrote: post #68
ale wrote: post #37

Earlier quoted context omitted.

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.

I posted a link but don't want to spam HN more than I have. It is proof-of-concept. Seriously burns some tokens (~80k - ~200k) but doesn't require AI after to scrape and automate a website so if all the people at Browser Use, Browser Base, and every one pounding every website used it, I think, the net benefit would be in the billions. I would recommend using it in isolation. Nonetheless, it works very very well on my…

It sounds like this is along the lines of Firecrawl is trying to do? Or what Plaid has done for banking?

> I think, the net benefit would be in the billions.

I think, you must forgive people if they are somewhat hostile, if not sick and tired of these claims. It’s quite frustrating seeing individuals constantly saying things like this. Meanwhile I don’t think a lot of people are seeing the structural shifts that these claims imply. This is not an original idea. The disruption claim has been made for the past several years in various fields and the goalposts keep getting moved. AI will absolutely change and render some jobs moot even in its current state if Claude/GPT are able to make a profitable business model. If it turns out that Claude is really being subsidized by investors and it turns out that $200/month subscription is really a $5,000/month when Claude has to stand on its on, I’m not sure what’s going to happen.

It’s clear you’ve gotten some good, if expensive use out of AI, but I’m not sure that experience scales or if it will exist in 5 years.

Post reply on HN