← All repos

formal-conjectures

A collection of formalized statements of conjectures in Lean.

GitHubgoogle-deepmind.github.io/formal-conjectures/
formal-mathematicslean4
Browse cluster: Lean4 Formal Verification & Cryptography →
1,835commits
205contributors
6languages

Tech stack & purpose

Formal Conjectures is a repository that collects formalized statements of mathematical conjectures in Lean 4. The project organizes problems from diverse sources including classic problem collections like Erdős problems, research papers, arXiv preprints, mathematics textbooks, Wikipedia, and optimization problem lists. The codebase is structured with a main directory for formalizations, a utilities module that provides infrastructure like custom attributes and linters, and a ForMathlib section containing definitions and lemmas suitable for upstreaming to the Lean Mathlib library. Contributors are expected to follow detailed conventions for namespacing, categorization using attributes (such as marking problems as open research, solved research, or textbook-level), assigning AMS subject classifications, and maintaining code quality standards that align with Mathlib's style guidelines.

Community & reference links

Languages

Lean
94.5%
JavaScript
2.7%
Python
1.0%
HTML
0.9%
CSS
0.9%
Shell
0.1%

Contributors (top 30 of 205)