DeepSeek: Advancing theorem proving in LLMs through large-scale synthetic data

This must be one of the best applications for LLMs, as you can always automatically verify the results, or reject them otherwise, right?

Same with code generation.

But generating useless code, or proofs, just to discard them is hardly a consequence and externality free effort.

But you can far more easily scale llm generation compared to human researchers.