Hacker News with Generative AI: Theorem Proving

DeepSeek: Advancing theorem proving in LLMs through large-scale synthetic data (arxiv.org)
To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems.
LeanDojo: Theorem Proving in Lean Using LLMs (leandojo.org)
LeanDojo: Theorem Proving in Lean Using Language Models (leandojo.org)