[vatsachak]

Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yet

[p-e-w]

That’s true, they’re not great at it. Just better than 99.99% of humans.

[slopinthebag]

Source?

[p-e-w]

The fact that 99.99% of humans have never used a formal theorem prover?

[vatsachak]

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.

But every time I use Codex unless I specifically give it the abstractions it writes code that is way too specific.

[DavidSJ]

> 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]

You're right, forgot a factor of 10 whoops

[slopinthebag]

How do we know if they’re better or not if they haven’t used one?