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

121–130 of 208 posts

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

#121

Post by tossandthrow »

threethirtytwo wrote: post #105
tartoran wrote: post #103

Earlier quoted context omitted.

Humans needing to ask new question due to curiosity push the boundaries further, find new directions, ways or motivations to explore, maybe invent new spaces to explore. LLMs are just tools that people use. When people are no longer needed AI serves no purpose at all.

Who said LLMs can’t push boundaries either? People can use other people as tools. An LLM being a tool does not preclude it from replacing people. Ultimately it’s a volume problem. You need at least one person to initialize the LLM. But after that, in theory, a future LLM can replace all people with the exception of the person who initializes the LLM.

The initialization problem is solved - maybe the next Nobel price will be given to a Mac mini.

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

#122

Post by parineum »

in-silico wrote: post #115
ryanar wrote: post #81

Earlier quoted context omitted.

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…

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?

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

#123

Post by red75prime »

psychoslave wrote: post #38
TrainedMonkey wrote: post #7

Earlier quoted context omitted.

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.

Yeah. Great mathematicians were able to upgrade a "yan, tan, tethera" number system using pen and paper (or stylus and clay).

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

#124

Post by specvsimpl »

parineum wrote: post #122
in-silico wrote: post #115

Earlier quoted context omitted.

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…

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.

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

#125

Post by slopinthebag »

DrewADesign wrote: post #104
slopinthebag wrote: post #51

Earlier quoted context omitted.

We will come up with new jobs, like we have for all of human history. I think even in an abundance utopia people will still work - we need purpose to sustain our existence. The work will become even more fulfilling however.

Throughout human history that didn’t happen fast enough to avoid an astonishing amount of human misery. Nobody’s worried about the future of work. They’re worried about the people that rely on tech jobs for food, mortgage/rent, cancer treatments, elder care, retirement, et al. Look at what happened to the rust belt, coal country, etc. etc. etc.

I agree with you, IMO largely this is an affordability crisis though, which is fuelled by inflation. I don't really offer many solutions besides eliminating inflation. I apologise if that is insufficient (it is).

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

#126

Post by specvsimpl »

abcde666777 wrote: post #117
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.

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.

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

#127

Post by [deleted] »

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…

[deleted]

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

#128

Post by utopcell »

kelseyfrog wrote: post #96
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 of now, no models have solved a Millennium Prize Problem[1]. 1. https://mppbench.com/

This is the real Litmus test isn't it? There will be a deafening silence from critics when AI decides P vs NP.

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

#129

Post by raincole »

kelseyfrog wrote: post #96
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 of now, no models have solved a Millennium Prize Problem[1]. 1. https://mppbench.com/

Most Fields medals winners haven't either, except one.

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

#130

Post by qnleigh »

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?

Post reply on HN