Open-problem statements, with their sources attached.

Each statement record keeps the mathematical question, a dated status source, accessible references, and any pinned Lean formulation separate from proof verification.

“Open” is a dated source assertion. In these pinned sources, sorry marks an admitted statement, not a proof. Source indexing does not mean the formulation has been independently built or certified by Therefore.

Search open problemsFilter by mathematical fieldFilter by source collection

All topics

Search topics

Additive combinatoricsAlgebraic geometryAlgorithmsAMS 11AMS 12AMS 13AMS 14AMS 15AMS 16AMS 18AMS 20AMS 22AMS 26AMS 28AMS 3AMS 30AMS 32AMS 33AMS 35AMS 37AMS 40AMS 41AMS 42AMS 46AMS 47AMS 49AMS 5AMS 51AMS 52AMS 54AMS 57AMS 58AMS 6AMS 60AMS 68AMS 8AMS 81AMS 91AMS 94AnalysisArithmetic geometryAssociative algebrasAutomata theoryCalculus of variationsCategory theoryCombinatoricsCommutative algebraComplex analysisComplexity theoryComputationComputer scienceConvex geometryDesign theoryDiophantine approximationDiophantine equationsDiscrete dynamicsDivisorsDynamical systemsDynamicsElliptic curvesExponential equationsExtremal set theoryField theory and polynomialsFluid mechanicsFunctional analysisGeneral topologyGeometryGraph labelingGraph theoryGroup theoryHarmonic analysisHodge theoryJordan curvesLinear algebraMathematical logicMathematical physicsMathematicsMatrix theoryMeasure and integrationNormal numbersNumber theoryOperator theoryPartial differential equationsPerfect numbersPrime gapsPrime numbersProbabilityQuantum field theoryReal functionsSequences and seriesSet systemsSeveral complex variablesSieve theorySpecial functionsTheoretical computer scienceTopological groupsTopology

21 of 1194 statement records

17 source collections · 43 mathematical fields

Clear filters

Source labels openOEIS · Number theory

Primes of the form 2^n + 2^i + 1

*Conjecture (A81091)**: There are infinite primes of the form $2^n + 2^i + 1$ , with $0 < i < n$ .

Source checked Jul 26, 20261 pinned Lean statementInspect problem

1 2

Page 2 of 2

therefore

Search complete Lean declarations, inspect their provenance, and check code in a live Lean environment.

Research

Research proofs Open problems Search Mathlib Type and shape search Projects Researchers

Use Therefore

Check a proof Packages MCP, API, and editor Verification model

Built for the Lean community.Verification, provenance, and authorship stay separate.