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

101–110 of 208 posts

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

#101

Post by silentkat »

colechristensen wrote: post #29
dataviz1000 wrote: post #5

Earlier quoted context omitted.

I got Claude to self reference and update its own instructions to solve making a typed proxy API of any website. After a week, scores of iterations, it can reverse engineer any website. The first few days I had to be deeply involved with each iteration loop. Domain knowledge is helpful. Each time I saw a problem I would ask Claude to update its instructions so it doesn't happen again. Then less and less. Eventually i…

I have similar amounts of success (pretty good!) standing in line at a coffee shop talking to people who work for me through some action that needs to be taken and doing the same with AI. However I do not trust AI anywhere near as much as I trust the humans. The AI is super capable but also occasionally a psychopath toddler. I sat in amused astonishment when faced with job 2 not running because job 1 was failing Clau…

My work has required us all to be "AI Native". I am AI skeptical but am the type of person to try to do what is asked to the best of my ability. I can be wrong, after all.

There is some real power in AI, for sure. But as I have been working with it, one thing is very clear. Either AI is not even close to a real intelligence (my take), or it is an alien intelligence. As I develop a system where it iterates on its own contexts, it definitely becomes probabilistically more likely to do the right thing, but the mistakes it makes become even more logic-defying. It's the coding equivalent of a hand with extra fingers.

I'm only a few weeks into really diving in. Work has given me infinite tokens to play with. Building my own orchestrator system that's purely programmatic, which will spawn agents to do work. Treat them as functions. Defined inputs and defined outputs. Don't give an agent more than one goal, I find that giving it a goal of building a system often leads it to assert that it works when it does not, so the verifier is a different agent. I know this is not new thinking, as I said I am new.

For me the most useful way to think about it has been considering LLMs to be a probabilistic programming language. It won't really error out, it'll just try to make it work. This attitude has made it fun for me again. Love learning new languages and also love making dirty scripts that make various tasks easier.

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

#102

Post by arjie »

amelius wrote: post #35
marsten wrote: post #21

Earlier quoted context omitted.

In the grand scheme it's good to invent things that replace human labor. It frees up people to do more interesting things. The goal should be to put everyone out of a job.

> The goal should be to put everyone out of a job. Yeah, but why does it need to take the fun jobs first, like painting, writing poems, coding, making music, ... I want the AI to cook, do the dishes, take out the trash, etc.

Well, because consuming art, reading poems, having code written for you that solves a problem, and listening to music is also fun. Recently I wanted a grand elegy to Britain written as the Empire started failing and set to music in a specific style. I had it playing in the background while fixing some issues with some software.

It truly was joyful to have this available to me. It didn’t have to have mass appeal or need me to pay the right artists the right amounts. I had it in moments.

It’s a wonderful world.

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

#103

Post by tartoran »

threethirtytwo wrote: post #100
hodgehog11 wrote: post #88

Earlier quoted context omitted.

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.

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.

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

#104

Post by DrewADesign »

slopinthebag wrote: post #51
pixl97 wrote: post #23

Earlier quoted context omitted.

>It frees up people to do more interesting things Like beg on the corners and starve in the street? Trying to figure out how the basics of capitalism where labor is exchanged for money is not going to work well when the only jobs left are side gigs. Something will have to change and a lot of People will fight said change.

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.

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

#105

Post by threethirtytwo »

tartoran wrote: post #103
threethirtytwo wrote: post #100

Earlier quoted context omitted.

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.

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.

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

#106

Post by slopinthebag »

bitwize wrote: post #73
vatsachak wrote: post #53

Earlier quoted context omitted.

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

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…

Actually I will argue. Complex systems are akin to a graph, attributes of the system being the nodes and the relationships between those attributes being the edges. The type of mechanistic thinking you're espousing is akin to a directed acyclic graph or a tree, and converting an undirected cyclic graph into a tree requires you to disregard edges and probably nodes as well. This is called reductionism, and scientific reductionism is a cancer for understanding complex phenomena like sociology or economics, and I posit, software as well.

People and corporations have been trying for at least the last five decades to reduce software development to a mechanistic process, in which a system is understandable solely via it's components and subcomponents, which can then be understood and assembled by unskilled labourers. This has failed every time, because by reducing a graph to a DAG or tree, you literally lose information. It's what makes software reuse so difficult, because no one component exists in isolation within a system.

The promise of AI is not that it can build atomic components which can be assembled like my toaster, but rather that it can build complex systems not by ignoring the edges, but managing them. It has not shown this ability yet at scale, and it's not conclusive that current architectures ever will. Saying that LLM's are better than most professional programmers is also trivially false, you do yourself no favours making such outlandish claims.

To tie back into your point about creativity, it's that creativity which allows humans to manage the complexity of systems, their various feedback loops, interactions, and emergent behaviour. It's also what makes this profession broadly worthwhile to its practitioners. Your goal being to reduce it to a mechanistic process is no different from any corporation wishing to replace software engineers with unskilled assembly line workers, and also completely misses the point of why software is difficult to build and why we haven't done that already. Because it's not possible, fundamentally. Of course it's possible AI replaces software developers, but it won't be because of a mechanistic process, but rather because it becomes better at understanding how to navigate these complex phenomena.

This might be besides the point, but I also wish AI boosters such as yourself would disclose any conflict of interests when it comes to discussing AI. Not in a statement, but legally bound, otherwise it's worthless. Because you are one of the biggest AI boosters on this platform and it's hard to imagine the motivation of spending so much time hardlining a specific narrative just for the love of the game, so to speak.

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

#107

Post by slopinthebag »

bitwize wrote: post #98
abcde666777 wrote: post #79

Earlier quoted context omitted.

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.

That is akin to saying if you aren't using an IDE you are not working efficiently or employing industry best practice, which is insane when you consider people using Vi often run rings around people using IDEs.

AI usage is a useless metric, look at results. Thus far, results and AI usage are uncorrelated.

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

#108

Post by slopinthebag »

vatsachak wrote: post #61
slopinthebag wrote: post #59

Earlier quoted context omitted.

Yeah, it's hard to compare management and programming but they're both multimodal in very different ways. But there's gonna be entire domains in which AI dominates much like stockfish, but stockfish isn't managing franchises and there is no reason to expect that anytime soon. I feel like something people miss when they talk about intelligence is that humans have incredible breadth. This is really what differentiates…

Exactly. It's what the execs are missing. Also animals thrive in underspecified environments, while AIs like very specific environments. Math is the most specified field there is lol

Oooh yeah that's really good framing. Humans have been building machines that outperform humans for hundreds of years at this point, but all in problems which are extremely well specified. It's not surprising LLM's are also great in these well specified domains.

One difference between intelligence and artificial intelligence is that humans can thrive with extremely limited training data, whereas AI requires a massive amount of it. I think if anybody is worried about being replaced by AI, they should look at maximising their economic utility in areas which are not well specified.

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

#109

Post by DrewADesign »

drfloyd51 wrote: post #42
DowsingSpoon wrote: post #33

Earlier quoted context omitted.

I’ve thought about this myself. Couple of points: 1) It’s not my job to fix all the problems of Capitalism. It’s painful to try to fight the system without collective action. My family and I have to eat too. 2) We have had a solution all along for the particular problem of AI putting devs out of work. It’s called professional licensure, and you can see it in action in engineering and medical fields. Professional Soft…

It’s not your job to fix capitalism. But it is your job to evaluate if your money making skill comes at too high a price for others. Say you found a job shooting people in the head for money. Like if you work for ICE or something… You need to feed your family. Is this job ok? You may decide yes. I decided no. I will find another way to feed my family. You don’t get to escape consequences because you are a small cog i…

> But it is your job to evaluate if your money making skill comes at too high a price for others.

It’s not even the money-making skill: it’s the application of it. People that are good at shooting people can be beneficial to society as protectors or they can be the the business end of systemic oppression. People with software development skills don’t have to help optimize the motor in the brand-new shiny capitalism juicer.

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

#110

Post by DoctorOetker »

bitwize wrote: post #71
madrox wrote: post #66

Earlier quoted context omitted.

> I've always said this but AI will win a fields medal before being able to manage a McDonald's. I love this and have a corollary saying: the last job to be automated will be QA. This wave of technology has triggered more discussion about the types of knowledge work that exist than any other, and I think we will be sharper for it.

The ownership class will be sharper. They will know how to exploit capital and turn it into more capital with vastly increased efficiency. Everybody else will be hosed.

but what if we succeed in gamifying the latent knowledge in LLM's to upload it to our human brains, by some kind of speed / reaction game?
Post reply on HN