Formal Conjectures

Published subset · 7

Exact formalized conjecture occurrences from the upstream repository. This release includes seven rights-reviewed research open declarations; it is not the whole repository.

Open upstream repository Add a Result

Lean toolchain: v4.27.0
Source families: 3
Exact revision: 33c6a2dcafc5

Formalized conjecture occurrences

7 of 7

For every integer $x \ge 2$ there exists a prime between $x(x-1)$ and $x^2$ .
Oppermann.oppermann_conjecture.parts.iOppermann's Conjecture
Wikipedia
Research open
For every integer $x \ge 2$ there exists a prime between $x^2$ and $x(x+1)$ .
Oppermann.oppermann_conjecture.parts.iiOppermann's Conjecture
Wikipedia
Research open
Oppermann's Conjecture
Oppermann.oppermann_conjectureOppermann's Conjecture
Wikipedia
Research open
For statistical reasons it is conjectured that the sequence is finite. This is formalized as the assertion that for large enough $n$ , no valid zeroless power exists, which in our definition results in $a(n) = 0$ .
OeisA103662.conjectureOEIS A103662 open questions
OEIS
Research open
$a(40)$ , if it exists, is not known.
OeisA103662.conjecture.variants.a_40OEIS A103662 open questions
OEIS
Research open
Are prime numbers among sums of prime numbers distributed as $\frac n{2\ln(n)}$ ?
MathOverflow434111.restricted_prime_number_theorem
MathOverflow
Research open
Invariant Subspace Problem
InvariantSubspaceProblem.Invariant_subspace_problem
Wikipedia
Research open

Published subset boundary

All other declarations remain outside this published subset until their question-text retention, source locator, and occurrence identity are reviewed. Source categories and GitHub review status remain attributed upstream facts; they do not establish Vela scientific state.

Exact collection identity

Source commit: 33c6a2dcafc5e3cdebfc083203b0a051309ea5b4
Collection root: sha256:081ac179c36d0958b2b9f0e974984ccbd3db7f4798f8d957ff5aef5482dd7163

Formalized conjecture occurrences

Published subset boundary

Search problems.science