Skip to content

Home
Problems
- Erdős Problems
- Formal Conjectures
Updates

Problems

Problems

Published collections

Collection names qualify local identifiers; inclusion does not determine scientific truth.

Erdős Problems
The source-owned Erdős problem catalogue, with status, evidence, Results, and retained formalizations.
1,217 numbered · 2 with reviewed evidence
Formal Conjectures
A bounded rights-reviewed subset of exact research-open Lean declaration occurrences from the upstream collection.
7 published formalizations

Problems to explore

Recognizable starting points from both published collections.

Search all Problems

Erdős Problems

Suppose $n$ points in $\mathbb{R}^2$ determine a convex polygon and the set of distances between them is $\{u_1,\ldots,u_t\}$ . Suppose $u_i$ appears as the distance between $f(u_i)$ many pairs of points. Then $\sum_i f(u_i)^2 \ll n^3.$
Source says proved (Lean)4 formal declarations1 reviewed Resultvia Formal Conjectures
What is the largest $A\subseteq\{1,\dots,N\}$ such that all subset sums $\sum_{n\in S}1/n$ (over $S\subseteq A$ ) are distinct?
Source says solved6 formal declarations1 reviewed Resultvia Erdős Problems
If $A\subseteq\{1, ..., N\}$ with $|A| = n$ is such that the subset sums $\sum_{a\in S}a$ are distinct for all $S\subseteq A$ then $N \gg 2 ^ n.$
Source says open8 formal declarationsvia Formal Conjectures

Formal Conjectures

Frontier Browse 7

For every integer $x \ge 2$ there exists a prime between $x(x-1)$ and $x^2$ .
Wikipedia · formalized occurrence
For every integer $x \ge 2$ there exists a prime between $x^2$ and $x(x+1)$ .
Wikipedia · formalized occurrence
Oppermann's Conjecture
Wikipedia · formalized occurrence

Privacy Terms Accessibility Contact