Ramanujan is a good analogy for this situation. Theories could be right/wrong, until there's a proof. Same with anything AI produces. There's always a "told you so" baked in with it's response.
Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
91–100 of 208 posts
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#92Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#93[dead]
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#94Earlier quoted context omitted.
Learn plumbing
There is no reason why market for plumbing will get much larger than it is now (which is not too large)
lowest quote I got to replace toilet and faucet in the kitchen (my parts, just installation) - $895 (5 quotes total). market for trades is exploding and will grow larger and larger as gen alpha and beyond knows what screwdriver is as much as they know what rotary phone is (they dont how to use either)
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#95I'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…
It will be heavily still reliant onexpert human input and interactions. Knuth is an expert, and know how to guide.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#96I'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].
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#97Earlier 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
The search space for the game of Go was also thought to be too large for computers to manage.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#98Earlier quoted context omitted.
But LLMs have proven themselves better at programming than most professional programmers. Don't argue. If you think Hackernews is a representative sample of the field then you haven't been in the field long enough. What LLMs have actually done is put the dream of software engineering within reach. Creativity is inimical to software engineering; the goal has long been to provide a universal set of reusable components…
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.
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#99https://xcancel.com/BoWang87/status/2037648937453232504
So many of the replies are clearly AI. “That’s not X — it’s Y.”
Re: Further human + AI + proof assistant work on Knuth's "Claude Cycles" problem
#100I'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.
But are you ok with the trendline of ai improvement? The speed of improvement indicates humans will only get further and further removed from the loop.
I see posts like your all the time comforting themselves that humans still matter, and every-time people like you are describing a human owning an ever shrinking section of the problem space.