Comment by magicalist
10 hours ago
I mean, let's say you spun up a swarm of agents to rewrite a large component of a well used open source library to be memory safe. You could dump it in a big PR and walk away (we all know how that would go), or you could try engaging, see if they're interested, write something up and see where it goes.
The biggest problem is, IMO, drivebys uninterested in actual results, just getting a check mark, and the equivalent of dropping a 200k line PR on people and expecting them to be interested and do the work for you. These are things many on HN are familiar with and know how to do better :)
> and the equivalent of dropping a 200k line PR on people
I can understand why the community is pissed. So now, lean proofs can be churned out at scale, and the community is left to decipher all of that slop into human understanding. There are bad actors with misaligned incentives coming in with drive-by proofs upending what the community holds dear which is to practice and propagate the art. I applaud them for this declaration.
To re-align incentives the following could happen. AI slop lean proofs are dumped unceremoniously into a lean dumpster, and what gets rewarded are results that could digested into human understanding - via the already followed human review process. Prizes are not given to lean proofs since anyone with sufficient compute can churn them out.