Hacker News with Generative AI: Theorem Proving

VictorTaelin: SupGen is a coding AI runs on 1 core CPU can prove theorems (twitter.com)
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)