Hacker News with Generative AI: Theorem Proving

Show HN: Formalizing Principia Mathematica using Lean (github.com/ndrwnaguib)
This project aims to formalize the first volume of Prof. Bertrand Russell’s Principia Mathematica using the Lean theorem prover.
Mathematics, Formal Verification, Theorem Proving, Logic
136 points by ndrwnaguib 14 hours ago | 29 comments
Efficient E-Matching for Super Optimizers (vortan.dev)
Modern theorem provers and optimizing compilers are built on an interesting concept: the ability to recognize when two things are equal, even if they look completely different.
Computer Science, Optimization, Theorem Proving, Software Engineering
19 points by todsacerdoti 7 days ago | 0 comments
VictorTaelin: SupGen is a coding AI runs on 1 core CPU can prove theorems (twitter.com)
Artificial Intelligence, Coding, Theorem Proving
38 points by hyperbrainer 96 days ago | 5 comments
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.
Artificial Intelligence, Theorem Proving, Math, Data Generation
186 points by hhs 194 days ago | 54 comments
LeanDojo: Theorem Proving in Lean Using LLMs (leandojo.org)
LeanDojo, Theorem Proving, AI, Programming
170 points by aseg 271 days ago | 53 comments
LeanDojo: Theorem Proving in Lean Using Language Models (leandojo.org)
Theorem Proving, Lean, Language Models, Artificial Intelligence
3 points by hendler 274 days ago | 0 comments