There's nothing about prove2me that couldn't have been coded just like any other huge coding project frontier models have proven themselves extremely good at doing. It just happened to have been made by humans.
> A fact that LLM hawks have categorically denied here before, with opposition naturally flagged.
Yeah, because before now there's been literally zero proof of an automated theorem prover scaffold around the LLMs being used, and big counterexamples and such being found, with raw chat logs available, where no such thing was used.
> Now they have it in writing.
Yeah, because now it's actually being done. They talk about it as a novel thing, because it is. You don't get to claim being "right all along" from this
Wrong. AlphaProof is much older, used Lean and a tree search for tactics just like ACL2.
They all steal from ACL2 without attribution in the current publication boiler room atmosphere. They get away with it because the AI Cult has information and publication dominance.
There was a brief period that used only language for toy IMO problems, but for serious work like FLT they apparently reverted to established approaches.
Literally many previous instance used one. Right from alphaevolve onwards.
I'm not some "LLM is just a next token predictor guy" (GP seems to have a thing against LLMs), but to use LLMs properly you genuinely do need a grounded verifier and a planner. Coding harnesses for example are exactly that.
For some plans, you can AR generate the search tree and that's what subagents being planned around by high level (LLM)agents and such are. Coding agents even with subagents are imperfect even on verifiable tasks only because of that. If you can put a human to simply guide it, it becomes a full system. This is what we all do today whenever we use codex. It's not something that is "never done before".
I also don't subscribe to the purist view which is taken by GP. I prefer to think in terms of concentration inequalities. P(failure rate > r) < epsilon. You get different levels of autonomy for different values of r for the planner and verifier each. If you have a good planner and a good verifier, r is very very small and it's super useful. Autonomy at a given r comes from how much of the planner and how much of the verifier is automated at that r. All levels of autonomy are economically useful. Many values of r are economically useful.
In this case of FLT, the verification was entirely automated using lean, and it is correct upto lean compiler bugs (so a very small r). The planner was essentially a maintained graph (afaik. Prove2me doesn't use A* or any heuristic/evolutionary methods to limit or prune the frontier), AND importantly - I'm not seeing anyone on HN mention this - some human nudges, literally, which nodes to open.
The way to make AI systems more useful is to build great verifiers and great planners, which is what many companies and startups are doing. LLMs are already really really good proposers due to excellent generalization (to be pedantic, multiple stacked specialisations), especially MoE models, making them amenable to proposing at every point in a vast search tree without any adaptation.
Yes, it is possible to do complex tasks purely AR, so long as you can AR simulate the search, which in the case of LLMs corresponds to verbalising the search tree[4]. This is trivially true. Can this be useful? Yes. Can a millenium prize problem be solved purely AR? Sure. It's a hard problem for humans, there is no reason it has to be difficult to reach in the conditional distributions of every future LLM. In the trivial limit, an LLM trained on the solution 100% you can sample it out. An LLM 2 generations behind that may have it at p=0.001, entirely reachable given a planner, but probably not AR. An LLM 1 generation behind may have it at p=0.05, plausibly reachable purely AR.
But the key question is: is `r` smaller or larger if you have a planner versus not? The answer there is obvious. Second, if you have a threshold `r` that decides usefulness, is the set of things you can autonomously do under that threshold higher with planners and verifiers? Again the answer is an obvious yes.
Copy pasting code from chatgpt repeatedly is worse than using a coding harness where it gets grounded feedback, LLM weights kept constant. Keeping the history of things and the overall plan that worked fixed and isolating LLMs to do subtasks is better than developing a whole database in one continuous context. In some cases, the overall plan "tree" can itself be entirely verbalised, but most commonly there is human modifications/steering.
Can pure-LLM coding harnesses with just verifiers one shot most e commerce sites including planning? Yes. But we want to do more with it than e commerce sites. Will it keep improving thus enabling us to do more and more complex things? No obvious reason for a fixed limit to exist in theory[1]. But at any point on the progress curve, using it with a harness always gives better results versus not. Concretely, with fable 5.1, using it without a harness could not prove FLT in reasonable token budgets [3]. However, it is possible for say, idk, GPT9, trained on this, to verbalise this whole proof tree, and also potentially generalize it to another open problem, purely AR, in a reasonable token budget[2]. This was how we got from gsm8k to FLT in the first place.
It's not a binary "AR is useless" "AR is all you need".
[1] the limits are mostly economic, and time is itself a limit, see https://news.ycombinator.com/item?id=49161078
Tl;dr diminishing returns of test time scaling. Noam brown also has a piece about this.
[2] if it's too many tokens that we run out of time or money literally, that is the limit described in [1]. It is not linear or constant scaling necessarily as described again in [1].
[3] [2] is why we have to add token budgets as another axis apart from r and the autonomy level.
I do highly unusual, off the beaten path projects with AI.
For instance, a game engine written entirely in LuaJIT, but allocating almost all data structures using CFFI, a very unusual, custom object-orientation DSL I designed myself, and that uses SDL3's SDL_gpu library to do all rendering, a ton of GLSL 4.6 compute shaders cross compiled to SPIR-V and Metal (which constraints what GLSL can be written), and is a hybrid tile-oriented and 3D engine.
Another example is my Emacs-like live-modifiable image-based editor, again in LuaJIT+CFFI, with a kqueue+atomic lock-free ring buffer+pthread based actor model, each running a separate LuaJIT interpreter, with a custom advicing system, event bus, async/await implementation riding on the event bus, a custom process management and IO library, and testing via Tmux.
Even DeepSeek V4 Flash mostly does fine with this, once it's built a few memories in the memory system. Let alone something like DSv4-Pro or GLM 5.2. All I can say is skill issue.
It's not an issue of usual vs unusual, I'm saying the models are way better at writing and maintaining django or react code bases than your own hand rolled architecture that you define in some docs that it has to learn and keep in context. All of the models do an amazing job making local edits and working in small greenfield projects but once you get to full production systems with close to a million lines things start to rot. The code still works and the models are able to make progress but all of a sudden you have 3-4 different versions of your concepts sprinkled in random corners of your code base.
My second point is that the models are way better at things like Rust or Lua than Python or JS, because the average person producing code in those languages has way more programming experience, so the code quality of training data online in those languages is higher than the programming 101 medium blogspam type content you see in more popular intro languages.
Did you actually manually review the 600k lines of code?
And the reason LLMs tend to produce such insanely large codebases is partially what the comment you're replying to explained, they duplicate everything all over the place.
The codebase is large because its a complex problem and its around 75% tests. Have used various tools to find duplicates and they arent there to any significant extent.
"You are violating the DRY principle with code like <blahblah>. Look through the codebase in depth, and identify possible places to consolidate common logic."
Yeah, there's no substitute for taste, but this is not that big of a deal. I infinitely prefer repeated code to crappy, leaky abstractions. Let the model generate some slop, then tighten it up either by hand or with more prompting.
I just finished an LLM assisted Rust rewrite of a production project after a couple months. It's around 150k LOC, mostly Rust, excluding generated code and tests. Around 200k if I include tests. I'm also now starting to extract / refactor some of it's code into their own reusable crates, so my LOC isn't going to grow and might even shrink a bit. I can't speak to 1M LOC, but I'd imagine that takes a lot of human context to reason about too, and you probably want to break it up into manageable chunks if possible.
LLMs have been a boon. I have a lot of guardrails in place though to keep the LLMs focused and producing correct and ergonomic code. A lot of effort and review has gone into creating these guardrails (choice of language, linting, forced conventions, tests, etc.). A lot of these practices will be useful in future projects. I highly recommend this approach. Don't just copy skills or processes that others publish. Figure it out yourself so the lessons stick. Human in the loop, especially one that has learned through practice and failure, is still immensely valuable IMO. It's a fine line between getting stuff done and yakshaving over your tooling... but that's always been the case, as proven by my vim dotfiles. :)
It's worth noting that the AI industry is filled with tons of snakeoil and BS. You don't need to take someone's course in "21 steps to be productive with AI" or w/e. Just like learning a new programming language, dig right in and try to build something that scratches an itch. Pick a project you have complete autonomy over instead of that "spend all the tokens" crap managers were pushing until recently (this has corrected now right?).
Parent saying "Skill issue" though... What a jackarse.
I haven't hit nearly a million lines, that's true, these projects are "only" 20k and 45k lines of code or so, respectively; however, I do have directed acyclic graphs of worker agents, managed asynchronously by the agent I chat directly with, do huge architectural refactors (the most recent, was to update everything in the codebase that used the sychronous Lua standard library `io` functions to use the asynchronous, multithreaded IO system I created for the editor — at least, everything that could use the new library, which I kept deliberately simple in a few ways, and everything that wasn't already temporary, but you know) and that's turned out quite well, and at least for me, 45k sloc is nothing to sneeze at, especially since with a green field project there's less examples to keep them on track. I do regularly check in to make sure it's using my design to the fullest, as well.
I don't necessarily disagree with the overall point you're making, but I think calling it a "skill issue" is a bit reductive. These are relatively new tools that are changing quickly, and the amount of flexibility in how you can use them is a lot higher than pretty much anything else we've built up patterns for in the industry in recent years. Rather than dismissing people who express having trouble producing the results you can, I feel like we should be giving lifting others up by providing insights into how we're able to do those things when we know that they're possible. Otherwise, how do we know it's truly a "skill" issue and not a "knowledge" issue, and the only thing stopping them is that no one has helped them understand?
In my experience, because as you say, the flexibility of these tools and how you engage with them is so broad, and how much the nuances of thay engagement can often matter, the only way to teach someone how to do what you do with them is to sit down and pair a program with them. Barring that, any instructions you could give would massively under-determined what they actually try as a result of your instructions, and so it ends up being an infinite loop of them just coming back and saying "it doesn't work." So in the end, people really just have to discover how these things work for themselves.
That's a completely reasonable take. I wouldn't have any issue with a nuanced comment like that. My issue with your above comment is that it's a lot more arrogant than nuanced.
That's fair, I think my point is there's a nuanced theory behind my choice to be rude, which is essentially "you need to experiment more, be more open minded, really work at it, and then you'll see what others are seeing, it isn't impossible." It's like Dark Souls, nobody can beat it for you, or teach you how to use dodge rolls, you've gotta build that skill yourself, and blaming the tools won't help.
I think your attitude is pretty lazy. It's a low-effort answer to say "skill issue" and then walk away feeling superior. Much harder to lean in to the other person, understand them, then help guide them onto the path. When you do this, you cause them to accelerate tremendously.
IMHO as you get more senior in software, after a while the only interesting metric becomes: are you raising the level of the people around you?
EDIT: looking at your Github seems like you are still in university. So I'll say "age and experience issue" on your end ;)
> IMHO as you get more senior in software, after a while the only interesting metric becomes: are you raising the level of the people around you?
Strongly agree, especially given how helping your teammates scales geometrically rather than linearly like improving your own output. If you work on a team team of five people with roughly equal output, and each becomes 20% more productive because of improvements you make, your team's output is increased the same as if you doubled your own productivity without helping anyone else on your team. (The math doesn't work out the same if your teammates aren't as productive as you already, but that's just an another argument for why it's better in the long run to be someone who can enable those around them rather than someone who only helps themself; helping everyone else has compounding returns if you keep doing it!)
I personally just also find it more fulfilling to be someone who makes everyone else around me better rather than just trying to be better than anyone else, but I recognize that not everyone will be motivated by that, so sometimes framing it in terms of raw output can help. The other potentially strong argument for those who are a bit more motivated by their own experiences only is that it's usually a lot more fun to have smart productive coworkers than ones who make you scoff and say "skill issue" to!
> That's fair, I think my point is there's a nuanced theory behind my choice to be rude, which is essentially "you need to experiment more, be more open minded, really work at it, and then you'll see what others are seeing, it isn't impossible."
Why not just say that then, instead of being rude? I pretty firmly disagree with the idea that being rude is ever a useful way to convey information rather than intent. Content and tone are separate axes that you can calibrate independently, so what you're saying is never an excuse for how you say it. Being rude conveys emotion, not information, and you didn't really convey information in your comment other than "look at how amazing the stuff I do is", and that's not a particularly effective mechanism for getting people to see your point of view.
I agree with you and I didn't think your comment was rude. Some people are against using LLMs and they will always find an excuse instead of experimenting with them so it doesn't matter how helpful you try to be they already made their mind.
> Some people are against using LLMs and they will always find an excuse instead of experimenting with them so it doesn't matter how helpful you try to be they already made their mind.
Do you think that I'm "against LLMs" and "finding an excuse instead of experimenting" because I disagree with you and the parent comment? If so, you should consider whether your perceptions are accurate, because I use them extensively.
More generally, if you aren't interested in engaging with the people who disagree with you, and you think that enough of them are arguing in bad faith and will never change their mind that their presence should determine the tone of your comments, why bother engaging in the discussion at all then?
I think "skill issue" is often deployed (including here) as a shortcut for what you said - "the only thing stopping them is that no one has helped them understand".
(I try not to say "skill issue" myself because it comes across as rude.)
It is easier to get an LLM to tell an unusual story using the most popular phrases than have it tell a common story using off-kilter uncommon phrases.
The big arc is easy to get using an LLM, getting it to do the details correctly, that is the actual hard part. So in my cases I (by other people's account a legendarily patient person) lost my cool trying to get a LLM to write CSS in a way that makes any sense if you have a design background. I ended up rewriting the whole CSS by hand, because it is inconsistent, piecemeal and just doesn't make sense. Yeah let's make everything bold and important. Yeah let's write internal implementation details into a label in the UI.
I decided to use LLMs as an aid to my own thinking, not as a replacement.
I regularly see claims by people that they have produced large, reliable bodies of code using vibe coding. Unfortunately, no vibe coded project I've used comes anywhere close to code reviewed by a human. Admittedly, my sample size is very small: things like claude-code, OpenClaw, and the occasional project I see mentioned here. But compared to the things I used regularly like GNU coreutils, Firefox, Linux, vim, git and the hundreds of other software projects I use daily, vibe coded apps are in a different ballpark. Vibe coded apps of a few 100k lines often glitch several times a day, the traditional ones that have several orders of magnitude more lines often don't fail in several years of use.
AI is now being used to assist in creating and maintaining these traditional bodies of software, of course. It looks like it has enhanced productivity as open source contributions have grown by 20% or so, and we've only just started to learn how to use it. I haven't noticed any degradation in quality. It may be too early to tell, but I suspect the engineers involved wouldn't let that happen.
As you say, it's a skill issue - it takes considerable skill to produce reliable maintainable code. But I suspect that wasn't the skill you are referring to.
Maybe the key difference is that you are so far off the beaten path that there simply are no examples of what you are doing that the models "want" to emulate?
I've also had reasonable success with the models generating fairly idiomatic Objective-Smalltalk, my own language of which there are likely few to no examples in the training data.
things you described are not "highly unusual" in the way gp comment is describing. you are just remixing bunch of stuff. Thats the type of thing ai is really good at.
The GP was just talking about not using common languages like TypeScript and frameworks like React, which is a bar of unusual that seems arguably far lower than mine, especially since I literally defined special custom DSLs with unusual semantics, and used libraries like SDL_gpu with little to no pre-existing training data. So this seems like shifting the goalposts.
"It's not an issue of usual vs unusual, I'm saying the models are way better at writing and maintaining django or react code bases than your own hand rolled architecture that you define in some docs that it has to learn and keep in context. All of the models do an amazing job making local edits and working in small greenfield projects but once you get to full production systems with close to a million lines things start to rot. The code still works and the models are able to make progress but all of a sudden you have 3-4 different versions of your concepts sprinkled in random corners of your code base.
My second point is that the models are way better at things like Rust or Lua than Python or JS, because the average person producing code in those languages has way more programming experience"
I know nothing about you or your code, but till you make your code + workflows public and have all of it reviewed / critiqued (so that other can replicate the performance), it's hard to accept it as a serious case study.
For all we know, this could just as well be a severe case of Dunning-Kruger.
Check out the /docs dir in the repos for each plan file and the language specs.
They are my 4th and 5th DSLs and I learned quite a bit along the way, most importantly how to separate a WASM runtime wired up to a Monaco editor “lsp” with the same crate for editor-services that works with the actual system binary LSP.
Feel free to peruse the repos! I follow compression-oriented programming, so there are places where the code is "insufficiently" DRY intentionally, as I feel out the precise use cases, and I explicitly made some other decisions (like a God editor object) for meta design reasons (I want it to be easy to modify the editor state from anywhere, just like in Emacs), so all I ask is that you review these without being excessively punative to prove your point.
I've found this to be more consistently the case than not. People almost never post their project and in the rare cases that they do, it's usually some shambling mess that doesn't actually function. They put together a keyword soup post that sounds good on an AI generated resume but falls apart upon investigation.
> People almost never post their project and in the rare cases that they do, it's usually some shambling mess that doesn't actually function
It's funny because you chose to target the one who is pro-AI, who has since posted their code, and not the GP who is against AI, who also didn't post any code to support his opinion that "it turns out the models don't care about your ideas and want to do what's popular in their training data".
Its hard not to feel insulted here. "Projects using AI like this don't exist, and if they do, they're broken and the people who made them have psychosis." However, although I haven't tested my projects cross machine, or cross platform yet (my editor only works on MacOS because it uses kqueue), I would be happy to take an unedited video demonstration of both, I assure you they both run.
Not specifically about the comment you replied to, but there has been an absolute Cambrian explosion of plausible sounding projects that use really complicated words that are just AI psychosis. Recently there was someone who posted a huge Lean proof on GitHub supposedly of proving P=NP. The problem is AI is really good at deluding people if that person doesn't have domain specific knowledge. AI severely makes dunning Kruger worse
Do you have any evidence for Valkey "widely replacing" Redis, instead of just rapidly gaining adoption as well? Additionally, it's important to clarify that the replacement was 100% over licensing issues — iirc predating the vibe coding entirely — not the use of AI to code, and that furthermore, no one has to my knowledge pointed to any flaws in the Redis codebase even correlated with AI use. So this is a disingenuous framing.
100% of the employers I worked for (one employee) never did that switch. The license did not affect us; we had nothing to do with AWS and the like, so we just continued using Redis like before. We already had our RPM builds, so whatever course distros took, we did not even care to look.
To be honest until today I thought Kafka was the popular go-to Redis replacement, as almost none of my employers used Redis for its original, intended purpose, namely being an in-memory key-value store. What they really wanted was RabbitMQ.
Sure, it costs less, and AWS is in a dominant position. Users here are playing the side of the bully since they don't care about what is right and wrong with the hyperscalers. "BSD is better than AGPL!" And give money to the wrong side of the history. Nor that I expected anything better, the single person has a given sensibility, the mass, as a whole, do whatever is in a given moment convenient or believed to be more pure (license wise). However thanks to that, you will see how little progresses we will have (and we are having) in the space of open source system software with very open licenses. Developers of software mostly are not happy to bring OSS to the success to see them used by hyperscalers to capture all the value. However I did it again, with DwarfStart, to release code under the BSD license: even in the current situation, I think it is better to give back than to have a personal gain, but this is a position that very little folks can afford to take.
However: this conversation is completely out of topic but people instead of talking about AI and code, which is a tabu, will move the conversation to personal attacks and shit like that.
I wish you'd chosen a "non free" fair source or open core license from the start.
Amazon has stolen enormous wealth from you and your collaborators.
People cheer for the hyperscalers even though AWS and GCP are not at all open source themselves, charge absurd margin, and do everything in their power to lock you in.
It's really unfortunate.
Thank you for Redis.
Hopefully AI gives them extra competition. There doesn't seem to be a moat for them yet apart from distribution. Hopefully that holds. The world needs competition and less concentration of power.
In order to really leverage a nonfree (proprietary) or more-free (AGPL/SSPL) license you have to have a substantial thing to protect. If you try to protect something trivial, your competition will just implement it themselves, unless your price is low enough to make that not worth it. Redis is relatively trivial, it is a REmote DIctionary Service. Amazon could have written their own Redis quite easily.
They didn't, because the idea is sufficiently non-obvious, but ideas are protected by patents, not copyright.
Even RMS recommended using LGPL in some cases to maximize overall freedom by not making your competitors copy it. In the case of Redis, GPL probably would've maximised freedom (but not revenue) as Amazon still could've used it and released any changes they made.
Valkey has diverged from Redis, gaining features like vector search and multithreading.
Thanks, I believe that as a whole choosing the BSD created a more positive effect, so I'm happy with that. It is just that it is really unfair to read a comment where people use ValKey to accuse you of AI slop :D It means that our community, and this site itself, is at this point really low quality. This will in turn discourage the many great folks that are here. A replacement is needed. But TLDR, I would release Redis again with the BSD license if I could go back in time.
I thought arenas were one of the simplest and most easy to deal with and conceptualize memory management strategies around. Arguably easy, even easier to understand and just as easy to manage as GC. Did they do something special?
MoE experts were likely trained independently / in a sparse format. Training anything beyond 2t on typical systems would be infuriantingly slow, you could do 4t on nvidias room-scale solution, but for a reasonable training speed / batch size it caps around 3t.
concept is similar to how it works in inference, instead of performing regressive writes to the entire model you run the whole model, but part of the model can live in system memory and get swapped in/out on demand. So only XB parameters are active in training.
edit: I am not really sure if it works like that. I haven't looked too deep into deepseek v4 pro specifically.
The statistical methodology I used is mine. As is the interpretation. Completely. To the degree that I misunderstood statistics (and it is under debate even in the thread you link, and the people accusing me of misunderstanding statistics there are universally misrepresenting my point, which is to point out a total absence of evidence for any difference, not to prove the null hypothesis) that's on me
FWIW I understood your point just fine. It seemed to me that you made a clear enough distinction between "evidence that Claude didn't increase bugs" and "no good evidence either way".
It seems like based on e.g. [1] the article originally made some stronger claims about “no difference in bugs” that have been corrected. I agree that now it seems fine, but those edits might be why it feels like some commenters read a different article than you.
reply