3 ms·
Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yet
by vatsachak 3mo ago
Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yet
- p-e-w 3mo agoThat’s true, they’re not great at it. Just better than 99.99% of humans.
- slopinthebag 3mo agoSource?
- p-e-w 3mo agoThe fact that 99.99% of humans have never used a formal theorem prover?
- slopinthebag 3mo agoHow do we know if they’re better or not if they haven’t used one?
- vatsachak 3mo agoWorse than 0.01% of humans means that there are 8,000,000 people better than it. I know that's being pedantic I understand what you're saying. But every time I use Codex unless I specifically give it the abstractions it writes code that is way too specific.
- DavidSJ 3mo ago> Worse than 0.01% of humans means that there are 8,000,000 people better than it. I know that's being pedantic I understand what you're saying. Since we're being pedantic, it means that there are (approximately) 800,000 people better than it. ;)
- vatsachak 3mo agoYou're right, forgot a factor of 10 whoops