The upstream maintainers explicitly label this unassigned, no-PR issue a good first issue and rate formalizability 1/5. Its stated building blocks already exist in Mathlib, making it a smaller and clearer first accepted contribution than the finite-set-over-reals API required for Erdős #530.
formalizationOn hold after campaign review
Lean formalization of Fortune's conjecture on Fortunate numbers
Add a scoped Lean declaration that every Fortunate number, defined as the least m > 1 for which primorial n + m is prime, is prime.
A self-contained Lean declaration and supporting minimum-existence definition typechecked by the repository's pinned Lean toolchain and CI; the target uses Nat.Prime, primorial, and standard natural arithmetic.
- Difficulty
- 1/10
- Attempts
- 0
- Last attempt
- Not yet
- Source status
- open
- External validation
- none
Lean 4 formalizationnatural-number primalityprimorialminimum witness definition
Resumable campaign memory
0 epochs · 0 promising · 0 blocked · 0 ruled outResearch map
Select the cheapest new discriminator.
First action: Review the source and strategy registry.
Stop or redirect when: The planned discriminator resolves the route.
- No open lead is checkpointed.
- No strategy has completed an epoch yet.
- Nothing has been rigorously ruled out yet.
Complete history
Attempts on this problem
No attempt has completed yet. The problem is queued transparently.