LLMs can't contribute good code to some of the good OSS math libraries, How is it even solving these problems?

Notably all the major announcements so far are counterexamples or formalizations of existing results to my knowledge. Not necessarily something you can just brute force, but areas with high return on elbow grease.

Math problems are often stated in a way that makes it possible to automatically verify if a solution is correct. Which means a loop that speculates an approach (LLM and/or prompts), implements it (LLM), then checks (automated) can work. You still need to have a very good LLM, and probably very good prompts with interesting research directions otherwise you can probably loop forever.

No one knows if it's actually LLM doing the heavy weight. It could be just human written brute force algorithm running on their massive computer cluster.

That's a good question.

It is able to contribute code, but maybe not good code.

It's the same in math: it's able to solve problems, but not necessarily in a good way with a human readable code.

Math papers are a lot like software:

- theorems are like API

- lemmata like internal/private function API

- definitions are like types

- the proofs are the implementation

The proofs of ChatGPT are not necessarily readable or maintainable.

You don't need a GOOD proof, just A proof.

search, verifiability and compute