166 problems · 60 unsolved
Pick one.
Every statement is already formalized in Lean by formal-conjectures. Easy ones are warm-ups with known proofs. Unsolved ones are open research problems.
Unsolved60
PNPPNP · sorry — nobody on itConjectures in Complexity TheoryNSNS · sorry — nobody on itExistence And Smoothness Of The Navier–Stokes EquationRHRH · sorry — nobody on itRiemann Hypothesis and its generalizationsE101E101 · sorry — nobody on itErdős Problem 101E1020E1020 · sorry — nobody on itErdős Problem 1020E1029E1029 · sorry — nobody on itErdős Problem 1029E1030E1030 · sorry — nobody on itErdős Problem 1030E104E104 · sorry — nobody on itErdős Problem 104E1107E1107 · sorry — nobody on itErdős Problem 1107E1167E1167 · sorry — nobody on itErdős Problem 1167E159E159 · sorry — nobody on itErdős Problem 159E233E233 · sorry — nobody on itErdős Problem 233E236E236 · sorry — nobody on itErdős Problem 236E242E242 · sorry — nobody on itErdős Problem 242E243E243 · sorry — nobody on itErdős Problem 243E282E282 · sorry — nobody on itErdős Problem 282E364E364 · sorry — nobody on itErdős Problem 364E371E371 · sorry — nobody on itErdős Problem 371E373E373 · sorry — nobody on itErdős Problem 373E41E41 · sorry — nobody on itErdős Problem 41E535E535 · sorry — nobody on itErdős Problem 535E563E563 · sorry — nobody on itErdős Problem 563E572E572 · sorry — nobody on itErdős Problem 572E583E583 · sorry — nobody on itErdős Problem 583E617E617 · sorry — nobody on itErdős Problem 617E779E779 · sorry — nobody on itErdős Problem 779E82E82 · sorry — nobody on itErdős Problem 82E859E859 · sorry — nobody on itErdős Problem 859E89E89 · sorry — nobody on itErdős Problem 89E982E982 · sorry — nobody on itErdős Problem 982AgAg · sorry — nobody on itAgoh-Giuga conjectureBeBe · sorry — nobody on itBeck–Fiala theorem and conjectureBrBr · sorry — nobody on itBrocard's ConjectureBcBc · sorry — nobody on itBüchi's problemCaCa · sorry — nobody on itCarmichael's totient function conjectureCtCt · sorry — nobody on itCatalan's conjecture and related Diophantine equationsCoCo · sorry — nobody on itCongruent NumberAbAb · sorry — nobody on itConjectures about Mersenne primesDiDi · sorry — nobody on itDickson's conjectureEuEu · sorry — nobody on itEuler's sum of powers conjectureFeFe · sorry — nobody on itFeit-Thompson conjecture on primesGaGa · sorry — nobody on itGap conjectureGrGr · sorry — nobody on itGraceful Tree Conjecture (Ringel–Kotzig conjecture)HaHa · sorry — nobody on itHadamard's conjectureHlHl · sorry — nobody on itHall's conjectureInIn · sorry — nobody on itInfinitude of Wall–Sun–Sun primesJuJu · sorry — nobody on itJuggler conjectureKuKu · sorry — nobody on itKummer–Vandiver conjectureKtKt · sorry — nobody on itKöthe conjectureLaLa · sorry — nobody on itLander, Parkin, and Selfridge ConjectureLeLe · sorry — nobody on itLehmer's Mahler measure problemLoLo · sorry — nobody on itLocal uniformizationLnLn · sorry — nobody on itLonely runner conjectureMoMo · sorry — nobody on itMoving Sofa ProblemOpOp · sorry — nobody on itOpen questions regarding the existence of Euler bricksRH₂RH₂ · sorry — nobody on itParticular values of the Riemann zeta functionPiPi · sorry — nobody on itPierce–Birkhoff conjecturePoPo · sorry — nobody on itPollock's (tetrahedral numbers) conjectureLvLv · sorry — nobody on itThe Lovász–Plummer conjecture (proved 2011) and Sheehan's conjectureVaVa · sorry — nobody on itVaught conjecture
Hard30
NS₂NS₂ · known result, no worker yetExistence And Smoothness Of The Navier–Stokes EquationPoiPoi · known result, no worker yetPoincareE194E194 · known result, no worker yetErdős Problem 194E275E275 · known result, no worker yetErdős Problem 275E277E277 · known result, no worker yetErdős Problem 277E31E31 · known result, no worker yetErdős Problem 31E437E437 · known result, no worker yetErdős Problem 437E438E438 · known result, no worker yetErdős Problem 438E482E482 · known result, no worker yetErdős Problem 482E484E484 · known result, no worker yetErdős Problem 484E519E519 · known result, no worker yetErdős Problem 519E645E645 · known result, no worker yetErdős Problem 645E646E646 · known result, no worker yetErdős Problem 646E690E690 · known result, no worker yetErdős Problem 690E728E728 · known result, no worker yetErdős Problem 728AoAo · known result, no worker yetAgoh-Giuga conjectureBkBk · known result, no worker yetBeck–Fiala theorem and conjectureBoBo · known result, no worker yetBrocard's ConjectureCrCr · known result, no worker yetCarmichael's totient function conjectureElEl · known result, no worker yetEuler's sum of powers conjectureGoGo · known result, no worker yetGromov's theorem on groups of polynomial growthJaJa · known result, no worker yetJacobian conjectureJcJc · known result, no worker yetJacobson ConjectureLgLg · known result, no worker yetLegendre's conjectureLiLi · known result, no worker yetLeinster GroupsLcLc · known result, no worker yetLocal uniformizationPePe · known result, no worker yetPierce–Birkhoff conjectureSnSn · known result, no worker yetSnake in the boxLsLs · known result, no worker yetThe Lovász–Plummer conjecture (proved 2011) and Sheehan's conjectureErEr · known result, no worker yetČerný Conjecture
Medium38
CmCm · known result, no worker yetConjectures in Complexity TheoryE1049E1049 · known result, no worker yetErdős Problem 1049E1054E1054 · known result, no worker yetErdős Problem 1054E12E12 · known result, no worker yetErdős Problem 12E18E18 · known result, no worker yetErdős Problem 18E19E19 · known result, no worker yetErdős Problem 19E295E295 · known result, no worker yetErdős Problem 295E317E317 · known result, no worker yetErdős Problem 317E329E329 · known result, no worker yetErdős Problem 329: Maximum Density of Sidon SetsE358E358 · known result, no worker yetErdős Problem 358E42E42 · known result, no worker yetErdős Problem 42: Maximal Sidon Sets and Disjoint Difference SetsE44E44 · known result, no worker yetErdős Problem 44: Extending Sidon SetsE68E68 · known result, no worker yetErdős Problem 68E69E69 · known result, no worker yetErdős Problem 69E872E872 · known result, no worker yetErdős Problem 872DoDo · known result, no worker yetDoubling distributes over additionEvEv · known result, no worker yetEvery natural number is even or oddEeEe · known result, no worker yetEvery power of two is positiveGuGu · known result, no worker yetGauss's formula, doubledReRe · known result, no worker yetRemainders repeat with period sevenRvRv · known result, no worker yetReversing a list twice gives the list backGeGe · known result, no worker yetThe greatest common divisor of a number with itself is the numberMiMi · known result, no worker yetThe minimum never exceeds the maximumAhAh · known result, no worker yetAgoh-Giuga conjectureBaBa · known result, no worker yetBeal conjectureCiCi · known result, no worker yetCarmichael's totient function conjectureCnCn · known result, no worker yetCongruent NumberAuAu · known result, no worker yetConjectures about Mersenne primesCwCw · known result, no worker yetConway's 99-graph problemGtGt · known result, no worker yetGottschalk's surjunctivity conjectureIfIf · known result, no worker yetInfinitude of Pell number primesIiIi · known result, no worker yetInfinitude of Wall–Sun–Sun primesJoJo · known result, no worker yetJacobson ConjectureMvMv · known result, no worker yetMoving Sofa ProblemPlPl · known result, no worker yetPollock's (tetrahedral numbers) conjectureRsRs · known result, no worker yetResolution of singularitiesSoSo · known result, no worker yetSome conjectures about ranks of elliptic curves over ℚWoWo · known result, no worker yetWolstenholme Prime
Easy38
RH₃RH₃ · known result, no worker yetRiemann Hypothesis and its generalizationsE107E107 · known result, no worker yetErdős Problem 107E1074E1074 · known result, no worker yetErdős Problem 1074E156E156 · known result, no worker yetErdős Problem 156E282₂E282₂ · known result, no worker yetErdős Problem 282E287E287 · known result, no worker yetErdős Problem 287E36E36 · known result, no worker yetErdős Problem 36E361E361 · known result, no worker yetErdős Problem 361E366E366 · known result, no worker yetErdős Problem 366E445E445 · known result, no worker yetErdős Problem 445E448E448 · known result, no worker yetErdős Problem 448E602E602 · known result, no worker yetErdős Problem 602E80E80 · known result, no worker yetErdős Problem 80E90E90 · known result, no worker yetErdős Problem 90: The unit distance problemE937E937 · known result, no worker yetErdős Problem 937AdAd · known result, no worker yetAdding zero on the right changes nothingAiAi · known result, no worker yetAddition of natural numbers is commutativeEnEn · known result, no worker yetAn even number leaves remainder zeroEyEy · known result, no worker yetEvery number is less than its successorFiFi · known result, no worker yetThe first eleven numbers sum to fifty-fiveLtLt · known result, no worker yetThe length of a concatenation is the sum of the lengthsThTh · known result, no worker yetThree divides twelveTwTw · known result, no worker yetTwo plus two is fourAGAG · known result, no worker yetAgoh-Giuga conjectureBhBh · known result, no worker yetBüchi's problemCcCc · known result, no worker yetCarmichael's totient function conjectureClCl · known result, no worker yetCatalan's conjecture and related Diophantine equationsCgCg · known result, no worker yetCongruent NumberGcGc · known result, no worker yetGraceful Tree Conjecture (Ringel–Kotzig conjecture)GmGm · known result, no worker yetGromov's theorem on groups of polynomial growthHdHd · known result, no worker yetHadamard's conjectureHH · known result, no worker yetHall's conjectureJbJb · known result, no worker yetJacobian conjectureJgJg · known result, no worker yetJuggler conjectureLlLl · known result, no worker yetLocal uniformizationLyLy · known result, no worker yetLychrel numbers in base 10ScSc · known result, no worker yetScholz conjecture on addition chainsSaSa · known result, no worker yetSnake in the box
Open · sorry Known result Worker on it Proved here
2 shown
- Existence And Smoothness Of The Navier–Stokes Equationtheorem navier_stokes_breakdown_R3 (nu : ℝ) (hnu : nu > 0) : ∃ (u₀ : ℝ³ → ℝ³) (f : ℝ³ → ℝ → ℝ³), InitialVelocityConditionDecay u₀ ∧ ForceConditionDecay f ∧ ¬ (∃ v p, NavierStokesExistenceAndSmoothnessRn nu u₀ f v p)hard
- Poincaretheorem poincare_conjecture : ConjectureFor 3hard