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

Surprised by the negativity here. A 7B class model +- doubles gpt4 score and everyone goes “meh”?!?

The attitude that HN on the whole has towards AI is what you would expect from an existential threat to a very high paying career.

I was excited for that headline, but I didn't get a clear & fair sense of comparison, like how prompt engineered etc was the comparison, or a false comparison?

There was not enough detail to determine what was ultimately useful & truly better, if anything. So lessons learned near useless. Likewise, I could not tell how useful the fine-tuning was and why, vs basic other tricks that would avoid all this complexity. The work seems good, but I found almost no scientific value in the experimentation and reporting. So I can't comment because there is little to comment on that I normally would. We focus more on the coding & analysis side, logical QA on fuzzier questions, so I am genuinely curious, supportive, am informed, etc, but left frustrated and wanting my time back.

I've seen broadly 2 attitudes: a refusal to accept AI as an existential threat to a high paying career, and a belief that AI is an existential threat to a high paying career.

As with most things in life, the truth is likely somewhere boring in the middle.

Option 3 anyone who can add Ai to their career with be even more highly paid because of the productivity boost.

"Deepseek" gets very little hype here for some reason. There is this Deepseek Coder llm model, that was comparable to others at the time and could run locally. Like, zero hype.