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

Re:DeepSeek: Advancing theorem proving in LLMs through large... by llm_trw on Tuesday October 15, 2024 @07:59AM (#41847620)

Doesn't matter what the granularity of your proof step us you still need to understand what that proof step does to be a mathematician. You seem to mistake syntactic brevity for semantic meaning.

[ Parent | on HN ]

Re:DeepSeek: Advancing theorem proving in LLMs through large... by auggierose on Tuesday October 15, 2024 @01:39PM (#41851005)

Mathematicians do very large proof steps, and so can the computer these days. If you do something like (proof by auto: thm_1 thm_2 thm_3) and it goes through, then I know why the proof works (because of these theorems), and this is similar to how a mathematician understands something. Syntactic brevity is indeed an indicator that you understand the proof. The better you understand something, the more concise you can formulate and prove it.

[ Parent | on HN ]