Live data from Hacker News

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

twitter.com

151–160 of 208 posts

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

#151

Earlier quoted context omitted.

Learn plumbing

This is kindof the opposite? Man + AI > either man or AI. I'd say "learn to work with Claude" is the better lesson here.

[flagged]

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

#152
If you give 100 monkeys 100 guns and room full of building materials, how long will it take before they build a house?

How long will it take before they rob a bank?

If they do either of those things will the results have been intentional from the simian’s POV?

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

#153

Earlier quoted context omitted.

Stockfish's power comes from mostly search, and the ML techniques it uses are mainly about better search, i.e. pruning branches more efficiently.

The weights must still have some understanding of the chess board. Though there is always the chance that it makes no sense to us

There is no understanding, the weights are selected based on better fit. Our cells have no understanding of optics just because they have the eyes coded in their DNA.

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

#154
post #28
post #20

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 2-3 hours "walking" while having to check in every 5-10 minutes? If I have to check in every 5-10 minutes, I won't taste coffee or hear that there's good music playing.

Just Claude code a push notification feature then

How is this better?

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

#155

When I was younger I remember a point of demarcation for me was learning the 4chan adage “trolls trolling trolls”, and approaching all internet interactions with skepticism. While I have been sure that Reddit for a while has succumbed to being “dead internet”. This thread is another moment for me- I can no longer recognize who is a bot, and who has honest intentions.

That's not just a great insight, but one that's worth carrying with us. That's why I built RememberBuddy. It's the one place for you to store your every-day insights so you don't forget.

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

#156

out of curiosity, i wonder if people are taking stabs at p!=np

"our new grad student made progress on the combinatorics problem we posed!" "oh awesome let's see if he can solve p!=np!"

Yes, too many people here do not understand the distance between the problems the article is discussing (and LLMs have solved) and the big problems in math and CS.

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

#157

Earlier quoted context omitted.

Learn plumbing

This is kindof the opposite? Man + AI > either man or AI. I'd say "learn to work with Claude" is the better lesson here.

[flagged]

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

#158
post #155

When I was younger I remember a point of demarcation for me was learning the 4chan adage “trolls trolling trolls”, and approaching all internet interactions with skepticism. While I have been sure that Reddit for a while has succumbed to being “dead internet”. This thread is another moment for me- I can no longer recognize who is a bot, and who has honest intentions.

That's not just a great insight, but one that's worth carrying with us. That's why I built RememberBuddy. It's the one place for you to store your every-day insights so you don't forget.

What a great project idea, worth getting it clients. That's why I've build a platform for promoting young startapers to find theit niche audience. Give it a try and go to the moon!

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

#159
post #136

Earlier quoted context omitted.

The search space for the game of Go was also thought to be too large for computers to manage.

It still is [1]. [1] https://www.vice.com/en/article/a-human-amateur-beat-a-top-g...

The blind spot exploiting strategy you link to was found by an adverserial ML model...
Post reply on HN