FormalConjectures 1283 modules
The problem statements themselves, organised by the collection they come from.
arXiv 30 modules
- «0911.2077».Conjecture6_3
- «0912.2382».CurlingNumberConjecture
- «1102.4662».AtiyahSutcliffe
- «1104.1579».CunninghamChain
- «1308.0994».BoxdotConjecture
- «1601.03081».UniqueCrystalComponents
- «1609.08688».sIncreasingrTuples
- «2001.02665».RingelConjecture
- «2104.00502».BarkerSequence
- «2107.00295».IndependentDomination
- «2107.12475».CollatzLike
- «2208.14736».ZariskiCancellation
- «2209.04540».SpectralSetsAndWeakTiling
- «2303.01089».FurstenbergTimesPTimesQ
- «2402.13202».CirculantHadamard
- «2501.03234».ArithmeticSumS
- «2504.17644».Margulis
- «2602.05192».FirstProof4
- «2602.05192».FirstProof6
- «2604.08040».Conjecture5_5
- «2605.02731».DeanCycles
- «2605.12342».Conjecture1
- «2606.03696».BondyLongestCycles
- «2607.03582».LpRogersShephard
- «2607.05349».MicroscopicWeighting
- «2607.05739».TanArctanSum
- «2607.06396».AlonTarsi
- «2607.08366».MinModulus
- «math.0110202».BanachMazurRotation
- «math.0608009».PoissonConjecture
Books 9 modules
- BorweinSineSeries
- BugeaudDistributionModuloOne.IntDistanceDistribution
- BugeaudDistributionModuloOne.Problem10_4
- BugeaudDistributionModuloOne.Problem10_5
- BugeaudDistributionModuloOne.Problem10_6
- BugeaudDistributionModuloOne.Problem10_7
- BugeaudDistributionModuloOne.Problem10_8
- BugeaudDistributionModuloOne.Problem10_9
- UniformDistributionOfSequences.Equidistribution
Erdős Problems 681 modules
- «1»
- «10»
- «100»
- «1000»
- «1002»
- «1003»
- «1004»
- «1007»
- «1008»
- «101»
- «1014»
- «1020»
- «1022»
- «1023»
- «1026»
- «1028»
- «1029»
- «1030»
- «1034»
- «1035»
- «1036»
- «1037»
- «1038»
- «104»
- «1041»
- «1043»
- «1044»
- «1047»
- «1048»
- «1049»
- «105»
- «1050»
- «1051»
- «1052»
- «1054»
- «1055»
- «1056»
- «1057»
- «1059»
- «1060»
- «1061»
- «1062»
- «1063»
- «1064»
- «1065»
- «1067»
- «1068»
- «107»
- «1071»
- «1072»
- «1073»
- «1074»
- «1077»
- «108»
- «1080»
- «1082»
- «1083»
- «1084»
- «1085»
- «1088»
- «1089»
- «109»
- «1090»
- «1092»
- «1093»
- «1094»
- «1095»
- «1096»
- «1097»
- «1098»
- «11»
- «1101»
- «1102»
- «1104»
- «1105»
- «1106»
- «1107»
- «1108»
- «1109»
- «1110»
- «1113»
- «1119»
- «1121»
- «1125»
- «1126»
- «1128»
- «1133»
- «1135»
- «1136»
- «1137»
- «1138»
- «1139»
- «1141»
- «1142»
- «1145»
- «1146»
- «1148»
- «115»
- «1150»
- «1159»
- «1167»
- «1175»
- «1176»
- «1188»
- «119»
- «1190»
- «1192»
- «1193»
- «1196»
- «1199»
- «12»
- «120»
- «1201»
- «1203»
- «1206»
- «1207»
- «1209»
- «1210»
- «1212»
- «1214»
- «123»
- «124»
- «125»
- «126»
- «128»
- «13»
- «130»
- «134»
- «137»
- «138»
- «139»
- «14»
- «141»
- «142»
- «143»
- «145»
- «146»
- «15»
- «150»
- «152»
- «153»
- «154»
- «155»
- «156»
- «158»
- «159»
- «16»
- «160»
- «163»
- «164»
- «166»
- «168»
- «17»
- «170»
- «172»
- «175»
- «178»
- «18»
- «180»
- «181»
- «183»
- «184»
- «188»
- «189»
- «193»
- «194»
- «195»
- «196»
- «197»
- «198»
- «199»
- «2»
- «20»
- «200»
- «202»
- «203»
- «204»
- «205»
- «206»
- «208»
- «209»
- «212»
- «213»
- «214»
- «215»
- «218»
- «219»
- «22»
- «221»
- «224»
- «226»
- «228»
- «229»
- «23»
- «233»
- «234»
- «236»
- «238»
- «239»
- «24»
- «241»
- «242»
- «243»
- «244»
- «245»
- «246»
- «247»
- «248»
- «249»
- «25»
- «250»
- «251»
- «252»
- «253»
- «254»
- «257»
- «258»
- «259»
- «26»
- «260»
- «261»
- «263»
- «264»
- «266»
- «267»
- «268»
- «269»
- «272»
- «273»
- «274»
- «275»
- «276»
- «277»
- «279»
- «28»
- «280»
- «281»
- «282»
- «283»
- «285»
- «287»
- «288»
- «289»
- «290»
- «291»
- «295»
- «296»
- «298»
- «299»
- «3»
- «30»
- «302»
- «303»
- «304»
- «306»
- «307»
- «31»
- «312»
- «313»
- «314»
- «315»
- «316»
- «317»
- «318»
- «319»
- «32»
- «321»
- «322»
- «323»
- «324»
- «325»
- «326»
- «328»
- «329»
- «33»
- «330»
- «331»
- «332»
- «333»
- «337»
- «34»
- «340»
- «341»
- «342»
- «346»
- «347»
- «348»
- «349»
- «350»
- «351»
- «352»
- «353»
- «354»
- «355»
- «357»
- «358»
- «359»
- «36»
- «361»
- «363»
- «364»
- «366»
- «367»
- «369»
- «370»
- «371»
- «372»
- «373»
- «375»
- «376»
- «377»
- «379»
- «38»
- «383»
- «385»
- «386»
- «387»
- «389»
- «39»
- «390»
- «392»
- «394»
- «396»
- «397»
- «398»
- «399»
- «4»
- «40»
- «400»
- «401»
- «402»
- «403»
- «405»
- «406»
- «409»
- «41»
- «410»
- «412»
- «413»
- «414»
- «416»
- «417»
- «418»
- «419»
- «42»
- «421»
- «422»
- «423»
- «424»
- «426»
- «427»
- «428»
- «429»
- «43»
- «431»
- «433»
- «434»
- «435»
- «44»
- «442»
- «443»
- «445»
- «447»
- «448»
- «45»
- «450»
- «452»
- «453»
- «454»
- «455»
- «456»
- «457»
- «458»
- «459»
- «46»
- «462»
- «463»
- «464»
- «469»
- «47»
- «470»
- «473»
- «476»
- «477»
- «478»
- «479»
- «48»
- «480»
- «481»
- «484»
- «485»
- «486»
- «487»
- «488»
- «489»
- «491»
- «493»
- «494»
- «495»
- «497»
- «498»
- «499»
- «5»
- «50»
- «501»
- «502»
- «503»
- «505»
- «506»
- «507»
- «508»
- «509»
- «51»
- «510»
- «512»
- «513»
- «516»
- «517»
- «519»
- «52»
- «520»
- «521»
- «522»
- «532»
- «533»
- «535»
- «536»
- «537»
- «538»
- «539»
- «540»
- «541»
- «544»
- «545»
- «546»
- «547»
- «548»
- «549»
- «550»
- «551»
- «552»
- «56»
- «562»
- «563»
- «564»
- «566»
- «567»
- «568»
- «569»
- «57»
- «570»
- «571»
- «572»
- «579»
- «58»
- «582»
- «583»
- «587»
- «590»
- «591»
- «592»
- «593»
- «594»
- «595»
- «596»
- «598»
- «599»
- «6»
- «60»
- «600»
- «602»
- «609»
- «61»
- «613»
- «615»
- «617»
- «618»
- «619»
- «621»
- «623»
- «624»
- «628»
- «63»
- «633»
- «639»
- «64»
- «645»
- «646»
- «647»
- «648»
- «649»
- «65»
- «650»
- «653»
- «655»
- «659»
- «66»
- «660»
- «666»
- «67»
- «672»
- «674»
- «677»
- «678»
- «68»
- «680»
- «681»
- «683»
- «686»
- «688»
- «689»
- «69»
- «692»
- «694»
- «695»
- «697»
- «698»
- «699»
- «7»
- «70»
- «700»
- «701»
- «705»
- «707»
- «71»
- «713»
- «714»
- «723»
- «726»
- «727»
- «728»
- «729»
- «73»
- «730»
- «74»
- «740»
- «741»
- «742»
- «749»
- «75»
- «750»
- «751»
- «753»
- «755»
- «756»
- «757»
- «760»
- «762»
- «765»
- «769»
- «77»
- «770»
- «773»
- «774»
- «775»
- «779»
- «785»
- «786»
- «789»
- «79»
- «794»
- «796»
- «798»
- «80»
- «800»
- «812»
- «817»
- «818»
- «82»
- «821»
- «822»
- «825»
- «826»
- «828»
- «829»
- «830»
- «835»
- «839»
- «844»
- «845»
- «846»
- «847»
- «848»
- «849»
- «85»
- «850»
- «851»
- «853»
- «855»
- «857»
- «859»
- «86»
- «862»
- «865»
- «867»
- «868»
- «869»
- «87»
- «871»
- «872»
- «873»
- «881»
- «883»
- «884»
- «885»
- «886»
- «887»
- «888»
- «889»
- «89»
- «890»
- «891»
- «893»
- «897»
- «898»
- «899»
- «9»
- «90»
- «904»
- «905»
- «906»
- «907»
- «91»
- «912»
- «913»
- «914»
- «918»
- «92»
- «920»
- «921»
- «923»
- «927»
- «93»
- «930»
- «931»
- «932»
- «933»
- «936»
- «937»
- «938»
- «939»
- «94»
- «940»
- «942»
- «943»
- «944»
- «945»
- «946»
- «948»
- «949»
- «950»
- «951»
- «952»
- «955»
- «958»
- «959»
- «96»
- «961»
- «962»
- «965»
- «966»
- «967»
- «968»
- «97»
- «970»
- «971»
- «972»
- «973»
- «974»
- «975»
- «978»
- «979»
- «98»
- «982»
- «985»
- «986»
- «987»
- «99»
- «990»
- «996»
- «997»
Green's Open Problems 57 modules
Hilbert Problems 2 modules
LittProblems 1 modules
MathOverflow 13 modules
OEIS 227 modules
- «100434»
- «100474»
- «100475»
- «100478»
- «100800»
- «101779»
- «102371»
- «102722»
- «102847»
- «103151»
- «103311»
- «103425»
- «103662»
- «103885»
- «104320»
- «105020»
- «105033»
- «105210»
- «105565»
- «105720»
- «105751»
- «105801»
- «107247»
- «108»
- «108081»
- «108129»
- «108211»
- «108301»
- «108306»
- «108569»
- «108864»
- «108866»
- «109074»
- «109227»
- «109671»
- «109845»
- «109905»
- «109908»
- «109909»
- «110475»
- «110566»
- «110835»
- «110854»
- «111114»
- «111291»
- «112521»
- «112970»
- «113010»
- «113019»
- «113213»
- «113250»
- «113252»
- «113254»
- «113255»
- «113257»
- «113258»
- «113271»
- «113609»
- «114137»
- «114216»
- «114362»
- «1146»
- «114831»
- «115257»
- «115366»
- «11545»
- «1157»
- «116150»
- «117027»
- «117531»
- «117545»
- «119563»
- «119591»
- «120424»
- «1223»
- «129365»
- «130911»
- «135508»
- «1359»
- «141057»
- «145355»
- «153330»
- «157225»
- «157237»
- «159829»
- «160324»
- «166944»
- «167604»
- «167918»
- «175386»
- «176477»
- «17666»
- «179524»
- «179537»
- «180017»
- «181546»
- «1818»
- «182126»
- «182510»
- «185150»
- «185895»
- «194806»
- «211417»
- «22030»
- «224»
- «224515»
- «227582»
- «228143»
- «228828»
- «231201»
- «232174»
- «2326»
- «237271»
- «239957»
- «2407»
- «2426»
- «243106»
- «24356»
- «2454»
- «248802»
- «256012»
- «258667»
- «260194»
- «267581»
- «271591»
- «278070»
- «280831»
- «281976»
- «282779»
- «287616»
- «28859»
- «289411»
- «2897»
- «300997»
- «303639»
- «303656»
- «306424»
- «306477»
- «307865»
- «308734»
- «309132»
- «3161»
- «3162»
- «317940»
- «323557»
- «325046»
- «340737»
- «341254»
- «34693»
- «34694»
- «357513»
- «358684»
- «3625»
- «363102»
- «363347»
- «368692»
- «37274»
- «372761»
- «38098»
- «38107»
- «382590»
- «38552»
- «38771»
- «40»
- «41»
- «4290»
- «46969»
- «48153»
- «49473»
- «51293»
- «5153»
- «51903»
- «5258»
- «52709»
- «53000»
- «53067»
- «53175»
- «55487»
- «56777»
- «60841»
- «60957»
- «62567»
- «63880»
- «64169»
- «64313»
- «6697»
- «67599»
- «67720»
- «67857»
- «69004»
- «69922»
- «69923»
- «7013»
- «70518»
- «70823»
- «71524»
- «71532»
- «72200»
- «7406»
- «7468»
- «76141»
- «76495»
- «77408»
- «78590»
- «78680»
- «78729»
- «7918»
- «79727»
- «80101»
- «80170»
- «80326»
- «81091»
- «83753»
- «84046»
- «86766»
- «87207»
- «87455»
- «87571»
- «87719»
- «89026»
- «91591»
- «91669»
- «92243»
- «93456»
- «93818»
- «945»
- «96535»
OptimizationConstants 1 modules
Other 7 modules
Papers 32 modules
- BranchingVAS
- CardinalityLindelof
- CasasAlvero
- CatchUpConjecture
- Chvatal
- ClaudesCycles
- ConjugacyClassSizes
- DeGiorgi
- DegreeSequencesTriangleFree
- Dubner
- FusibleNumber
- Gourevitch
- HartshorneConjecture
- Homogenous
- KotzigConjecture
- Kurepa
- LatinSquare
- LatinTableau
- MonochromaticQuantumGraph
- NLSCritical
- PrimeTuples
- ReedOmegaDeltaChi
- RingelConjecture
- Rupert
- SerreUniformity
- SizeOrderConnectedDomination
- StrongSensitivityConjecture
- TuDengConjecture
- VoronovskajaTypeFormula
- WeaklyFirstCountable
- WeakTiling
- ZagierMZV
Subsets 2 modules
Wikipedia 158 modules
- ABC
- AgohGiuga
- Agrawal
- AlgebraicNormality
- AlmostPerfectNumbers
- AmicableNumbers
- AndrewsCurtis
- Andrica
- ArtinPrimitiveRootsConjecture
- BalancedPrimes
- BatemanHornConjecture
- BealConjecture
- BeckFialaConjecture
- BetrothedNumbers
- BingBorsuk
- Bloch
- BorsukConjecture
- BoundedBurnsideProblem
- Brennanconjecture
- BrocardConjecture
- BrocardProblem
- Buchi
- Bunyakovsky
- BusyBeaver
- CarmichaelTotient
- Catalan
- CernyConjecture
- ClassNumberProblem
- CollatzConjecture
- CongruentNumber
- conjecture_1_3_to_2_3
- Conway99Graph
- DedekindNumber
- DeterminantalConjecture
- DiameterSimpleFiniteGroups
- Dickson
- DiophantineTuple
- ElliottHalberstamConjecture
- EllipticCurveRank
- ErdosMoser
- ErdosRadoSunflowerConjecture
- Euclid
- EulerBrick
- EulerSumOfPowers
- Exponentials
- FactorialPrime
- Falconer
- FeitThompsonPrimeConjecture
- Fermat
- FermatCatalanConjecture
- FibonacciPrimes
- Firoozbakht
- FlintCooksonHills
- FortuneConjecture
- Fuglede
- GapConjecture
- GaussCircleProblem
- Gilbreath
- GoldbachConjecture
- GoodmanConjecture
- Goormaghtigh
- GracefulLabeling
- Grimm
- GromovPolynomialGrowth
- Hadamard
- HadwigerNelson
- Hall
- HappyEndingProblem
- HardyLittlewood
- HerzogSchonheimConjecture
- HilbertFifthProblem
- IdonealCompleteness
- InscribedSquare
- InvariantSubspaceProblem
- InverseGalois
- Irrational
- JacobianConjecture
- Jacobson
- JugglerConjecture
- Kakeya
- Kaplansky
- Koethe
- KomlosConjecture
- KummerVandiver
- LanderParkinAndSelfridgeConjecture
- LegendreConjecture
- LehmerMahlerMeasureProblem
- LehmerTotient
- LeinsterGroup
- Lemoine
- LittlewoodConjecture
- LonelyRunnerConjecture
- LovaszPlummerConjecture
- LychrelNumbers
- MagicSquares
- Mahler32
- Mandelbrot
- MeanValueProblem
- Mersenne
- Mills
- MinimalOverlapProblem
- ModularityConjecture
- MoserWorm
- MovingSofa
- NoetherProblem
- NormalityOfPi
- NoThreeInLineProblem
- OddWeirdNumber
- Oppermann
- PebblingNumberConjecture
- Pell
- PerfectNumbers
- PierceBirkhoff
- PierpontPrime
- PollocksConjecture
- PolyTimeFunctions
- PompeiuProblem
- PowerfulNumbersDensity
- PrimesAndPerfectSquares
- PrimeTriplets
- QuasiperfectNumbers
- RamanujanTau
- RamseyNumbers
- RationalDistanceProblem
- RegularPrimes
- RiemannZetaValues
- RudinsConjecture
- SatoTateConjecture
- Schanuel
- Schinzel
- ScholzConjecture
- Selfridge
- Sendov
- SidorenkoConjecture
- SierpinskiNumber
- Singmaster
- SixStandardDeviations
- SnakeInTheBox
- SolitaryNumber
- SparseRuler
- SquarePacking
- SteinerSystem
- SumOfThreeCubes
- Superperfectnumbers
- SurjunctiveGroup
- Taxicab
- Toronto
- Transcendental
- TwinPrimes
- UnionClosed
- VaughtConjecture
- VizingConjecture
- WallSunSun
- WieferichMirimanoffPrime
- WieferichPrime
- WilsonPrime
- WolstenholmePrime
- WoodalPrimes
Written on the Wall II 49 modules
- «160»
- GraphConjecture1
- GraphConjecture100
- GraphConjecture101
- GraphConjecture103
- GraphConjecture109
- GraphConjecture13
- GraphConjecture133
- GraphConjecture141
- GraphConjecture142
- GraphConjecture143
- GraphConjecture144
- GraphConjecture145
- GraphConjecture146
- GraphConjecture16
- GraphConjecture17
- GraphConjecture18
- GraphConjecture19
- GraphConjecture194
- GraphConjecture198a
- GraphConjecture2
- GraphConjecture20
- GraphConjecture200
- GraphConjecture217
- GraphConjecture23
- GraphConjecture291
- GraphConjecture3
- GraphConjecture31
- GraphConjecture314
- GraphConjecture315
- GraphConjecture316
- GraphConjecture32
- GraphConjecture322
- GraphConjecture327
- GraphConjecture33
- GraphConjecture34
- GraphConjecture36
- GraphConjecture4
- GraphConjecture40
- GraphConjecture5
- GraphConjecture58
- GraphConjecture59
- GraphConjecture6
- GraphConjecture61
- GraphConjecture63
- GraphConjecture65
- GraphConjecture7
- GraphConjecture85
- Test
FormalConjecturesForMathlib 184 modules
Definitions and lemmas that the statements need but Mathlib does not yet have; candidates for upstreaming.
Algebra 12 modules
AlgebraicGeometry 4 modules
Analysis 9 modules
Combinatorics 61 modules
- Additive.Basis
- Additive.Convolution
- Additive.Coset
- Additive.DifferenceBasis
- Additive.RestrictedSumset
- Additive.VCDim
- AP.Basic
- Basic
- Digraph.Tournament
- Hypergraph.ThreeUniform
- LatinSquare
- LimitObjects.Graphon
- LimitObjects.Tournamenton
- Ramsey
- Ramsey.Diagonal
- SetFamily.PropertyB
- SetFamily.Sunflower
- SetFamily.UnionFree
- SetFamily.VCDim
- SetTheory.PartitionRelation
- SimpleGraph.AnnihilationNumber
- SimpleGraph.Balanced
- SimpleGraph.Circumference
- SimpleGraph.Clique
- SimpleGraph.Coloring.Vertex
- SimpleGraph.CompleteGraphEdgeCount
- SimpleGraph.Connectivity
- SimpleGraph.Cvetkovic
- SimpleGraph.Cycle
- SimpleGraph.CycleRank
- SimpleGraph.Decomposition
- SimpleGraph.Degeneracy
- SimpleGraph.Degrees
- SimpleGraph.DiamExtra
- SimpleGraph.Domination
- SimpleGraph.Eccentricity
- SimpleGraph.EdgeColouring
- SimpleGraph.FractionalAlpha
- SimpleGraph.HomDensity
- SimpleGraph.Hypercube
- SimpleGraph.Independence
- SimpleGraph.Induced
- SimpleGraph.Johnson
- SimpleGraph.LargestInducedTree
- SimpleGraph.LovaszTheta
- SimpleGraph.Matching
- SimpleGraph.PathCover
- SimpleGraph.Prod
- SimpleGraph.QuasiLineGraph
- SimpleGraph.Ramsey
- SimpleGraph.Residue
- SimpleGraph.SizeRamsey
- SimpleGraph.SpanningTree
- SimpleGraph.SubgraphIsomorphism
- SimpleGraph.SzegedIndex
- SimpleGraph.Temperature
- SimpleGraph.UnitDistancePlaneGraph
- SimpleGraph.VertexDistance
- SimpleGraph.WellTotallyDominated
- SimpleGraph.WienerIndex
- YoungDiagram
Computability 7 modules
Data 24 modules
- Bool.Basic
- Finset.Card
- Finset.Powerset
- Finset.ReciprocalSum
- Int.IntermediateValue
- Int.Order.Basic
- Nat.Factorization.Basic
- Nat.Full
- Nat.Init
- Nat.MaxPrimeFac
- Nat.PerfectPower
- Nat.Prime.Composite
- Nat.Prime.Defs
- Nat.Prime.Finset
- Nat.Prime.Infinite
- Nat.Squarefree
- Real.Constants
- Real.NearestInt
- Set.Density
- Set.Interval
- Set.Triplewise
- Sym.Sym2
- ZMod.Fp
- ZMod.PerfectDifferenceSet
FieldTheory 1 modules
Geometry 5 modules
GroupTheory 1 modules
Lean 1 modules
LinearAlgebra 3 modules
Logic 1 modules
NumberTheory 29 modules
- AdditionChain
- AdditiveComplement
- AdditivelyComplete
- AlmostPrime
- Amicable
- AutomorphicForm.BorelJacquet
- AutomorphicForm.BorelJacquet.CenterAction
- AutomorphicForm.BorelJacquet.LieDeriv
- AutomorphicForm.BorelJacquet.Subgroups
- BeurlingPrimes
- Carmichael
- CoveringSystem
- DiophantineApproximation.ZNumber
- DirichletCharacter.Basic
- Divisors
- Harmonic
- Lacunary
- LegendreSymbol.Basic
- NormalNumber
- NumberField.FundamentalDiscriminant
- NumberField.Quadratic
- PisotNumber
- PracticalNumbers
- PrimeGap
- Primitive
- SierpinskiNumber
- SmoothScale
- WallSunSunPrimes
- WieferichPrime
Order 7 modules
Probability 1 modules
RingTheory 4 modules
SetTheory 3 modules
Tactic 1 modules
FormalConjecturesUtil 23 modules
Attributes, linters, and metadata infrastructure used by the problem files.