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

81–90 of 208 posts

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

#81

Post by ryanar »

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…

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.

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

#82

Post by myffical »

vatsachak wrote: post #40
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…

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…

Some DeepMind researchers used mechanistic interpretability techniques to find concepts in AlphaZero and teach them to human chess Grandmasters: https://www.pnas.org/doi/10.1073/pnas.2406675122

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

#83

Post by hodgehog11 »

ryanar wrote: post #81
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…

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.

It's finding constructions and counterexamples. That's different from finding new proof techniques, but still extremely useful, and still gives way to novel findings.

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

#84

Post by frizlab »

ChrisClark wrote: post #75
frizlab wrote: post #15

Earlier quoted context omitted.

> I would go for a 2 or 3 hour walk with my phone using the remote control feature looking every 5 - 10 minutes to make sure it doesn't need human help. That is a nightmarish scenario tbh

So sitting at a desk is nicer than a walk outside for you? Why would relaxation be a nightmare?

Checking one’s phone every 5 to 10 minutes is nothing but relaxation. One needs to have the mind at ease to relax.

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

#85

Post by throw3747488 »

smokel wrote: post #39
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 think this is mostly about existing legislature, not about technology. In any other context than when your paycheck depends on it, you would probably not be following orders from a random manager. If your paycheck depended on following the instructions of an AI robot, the world might start to look pretty scary real soon.

AI actually has to follow all rules, even the bad rules. Like when autonomous car drives super carefully.

Imagine mcdonald management would enforce dog related rules. No more filthy muppets! If dog harasses customers, AI would call cops, and sue for restraining order! If dog defecates in middle of restaurant, everything would get desinfected, not just smeared with towels!

Nutters would crucify AI management!

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

#86

Post by hodgehog11 »

vatsachak wrote: post #53
slopinthebag wrote: post #46

Earlier quoted context omitted.

> AI will win a fields medal before being able to manage a McDonald's Of course, because it takes multi-modal intelligence to manage a McDonalds. I.e. it requires human intelligence. > I predict that in the future people will ditch LLMs in favor of AlphaGo style RL Same for coding as well. LLM's might be the interface we use with other forms of AI though.

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 groups can require representation by grid diagrams, and we know from ARC-AGI that LLMs don't do great with this.

Programming does not have this issue to the same extent; arguably, it involves the subset of maths that is exclusively problem solving using standard representations. The issues with programming are primarily on the difficulty with handling large volumes of text reliably.

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

#87

Post by hodgehog11 »

vatsachak wrote: post #40
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…

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

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

#88

Post by hodgehog11 »

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.

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

#89

Post by breatheoften »

Like so many things -- the evolution of AI math will I think follow trajectories hinted at in the 90s by the all time great sci-fi author Greg Egan. The nature of math won't change -- but the why of it definitely will. Egan imagined a future ai civilization in Diaspora where "math discovery" -- by nature in the future perhaps accurately described as "mechanistic math discovery" is modeled by society as a kind of salt mine environment in which you can dig for arbitrarily long amounts of time and find new nuggets. The nuggets themselves have a kind of "pure value" as mathematical objects even if they might not have any knowable value outside the mines. Some personalities were interested in and valued the nuggets for their own sake while others didn't but recognized that there were occasionally nuggets found in the mind that had broader appeal.

Research institutes like those founded by Terence Tao in our current present feel like they will align to this future almost perfectly on a long enough timeline -- tho I think on a shorter timeline this area of research is almost certain to provide a ton of useful ways to advance our current ai systems as our current systems are still in a state where literally anything that can generate new information that is "accurate" in some way -- like our current theorem prover engines are enormously valuable parts of our still manually curated training loops.

Post reply on HN