# google-deepmind/formal-conjectures

A collection of formalized statements of conjectures in Lean.

Repository: https://github.com/google-deepmind/formal-conjectures
Canonical: https://ross.abutalabs.com/products/formal-conjectures
Homepage: https://google-deepmind.github.io/formal-conjectures/
Language: Lean
License: Apache-2.0
License Family: permissive
Topics: formal-mathematics, lean4
Last push: 2026-09-02T22:10:54+00:00

## Health v2 (maintenance only)
Score: 70/100 (v2, computed 2026-09-03T02:20:16.233290+00:00)
- activity 100, release rhythm 51, longevity 34
- inputs: {"age_days": 478, "days_push": 0, "days_rel": 119, "gap_med": null, "n_releases_24m": 1}
- flags: none
- formula: round(0.45*activity + 0.35*rhythm + 0.20*longevity); archived -> min(score, 10)

## Adoption (not part of the score)
Stars 1221, forks 438 (observed 2026-09-03T02:15:12.383375+00:00)

## What it is
A curated collection of formalized statements of open mathematical conjectures written in Lean 4 using Mathlib, maintained by Google DeepMind. It provides thousands of precisely stated conjectures (e.g., from Erdős problems, Millennium Prize Problems, OEIS) intended as benchmarks for automated theorem provers and as a resource for the formal mathematics community.

## Use cases
- benchmark automated theorem provers on open conjectures
- find formal Lean statements of famous unsolved math problems
- clarify the precise meaning of a conjecture through formalization
- identify missing Mathlib definitions to contribute
- train or evaluate AI systems on formal mathematics tasks
- browse conjectures by subject area or source

## When to choose
- you need machine-checkable statements of open mathematical conjectures in Lean 4
- you are building or evaluating automated theorem proving or formalization tools
- you want to contribute formalizations to the Lean/Mathlib ecosystem
- you need a dataset of formal math problem statements for AI research

## When to avoid
- you need proved theorems rather than unproven conjecture statements
- you want an interactive theorem prover or proof assistant itself (use Lean/Mathlib)
- you need informal, human-readable problem collections without formalization
- your work does not involve Lean 4 or formal mathematics

## Facets
- artifact type: dataset
- maturity: active
- function: machine-learning, documentation, developer-tools
- domain: mathematics, education, artificial-intelligence
- platform: cross-platform
- tags: lean4, formal-mathematics, mathlib, conjectures, theorem-proving, benchmark, automated-theorem-proving, algorithms

## Member repositories
- google-deepmind/formal-conjectures (main) score 70

## Provenance
- Observed fields: from GitHub, fetched 2026-09-03T02:15:12.383375+00:00.
- Health v2: computed from the inputs above; adoption is never an input.
- Inferred fields (summary, facets, guidance): AI-extracted, prompt v1, taxonomy v1, on 2026-08-30T06:20:41.242202+00:00, confidence not recorded.
  - readme: https://github.com/google-deepmind/formal-conjectures (fetched 2026-09-03T02:15:12.383375+00:00, sha 9275100d6223)
  - homepage: https://google-deepmind.github.io/formal-conjectures/ (fetched 2026-08-29T12:27:46.791166+00:00, sha 806f7ed56406)
- Data as of 2026-08-30T08:39:29.467469+00:00.