Proof-Wanted/lakefile.lean at main · MathNetwork/Proof-Wanted · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
import Lake
open Lake DSL

package «formalization-candidates» where
  leanOptions := #[⟨`autoImplicit, false⟩]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4" @ "master"

-- Known theorems

lean_lib SL2RTraceClassification where
  srcDir := "candidates/known-theorems/sl2r-trace-classification"
  roots := #[`Statement]

lean_lib SL2RHomogeneousSpace where
  srcDir := "candidates/known-theorems/sl2r-homogeneous-space"
  roots := #[`Statement]

lean_lib CayleyTransform where
  srcDir := "candidates/known-theorems/cayley-transform"
  roots := #[`Statement]

lean_lib CantorSetDimH where
  srcDir := "candidates/known-theorems/cantor-set-dimh"
  roots := #[`Statement]

lean_lib BesicovitchCovering where
  srcDir := "candidates/known-theorems/besicovitch-covering"
  roots := #[`Statement]

lean_lib SardTheorem where
  srcDir := "candidates/known-theorems/sard-theorem"
  roots := #[`Statement]

lean_lib CoareaFormula where
  srcDir := "candidates/known-theorems/coarea-formula"
  roots := #[`Statement]

lean_lib AzumaHoeffding where
  srcDir := "candidates/known-theorems/azuma-hoeffding"
  roots := #[`Statement]

lean_lib Kolmogorov01 where
  srcDir := "candidates/known-theorems/kolmogorov-01"
  roots := #[`Statement]

lean_lib PoincareInequality where
  srcDir := "candidates/known-theorems/poincare-inequality"
  roots := #[`Statement]

lean_lib LaxMilgram where
  srcDir := "candidates/known-theorems/lax-milgram"
  roots := #[`Statement]

lean_lib RellichKondrachov where
  srcDir := "candidates/known-theorems/rellich-kondrachov"
  roots := #[`Statement]

lean_lib MaximumPrincipleHarmonic where
  srcDir := "candidates/known-theorems/maximum-principle-harmonic"
  roots := #[`Statement]

lean_lib WassersteinMetric where
  srcDir := "candidates/known-theorems/wasserstein-metric"
  roots := #[`Statement]

lean_lib KantorovichDualityDiscrete where
  srcDir := "candidates/known-theorems/kantorovich-duality-discrete"
  roots := #[`Statement]

lean_lib OptimalCouplingExistence where
  srcDir := "candidates/known-theorems/optimal-coupling-existence"
  roots := #[`Statement]

-- Open conjectures

lean_lib FranklSemimodular where
  srcDir := "candidates/open-conjectures/frankl-semimodular"
  roots := #[`Statement]

lean_lib DavenportRankTwo where
  srcDir := "candidates/open-conjectures/davenport-rank-two"
  roots := #[`Statement]

lean_lib ErdosStraus where
  srcDir := "candidates/open-conjectures/erdos-straus"
  roots := #[`Statement]

lean_lib SunflowerConjecture where
  srcDir := "candidates/open-conjectures/sunflower-conjecture"
  roots := #[`Statement]

lean_lib ChvatalConjecture where
  srcDir := "candidates/open-conjectures/chvatal-conjecture"
  roots := #[`Statement]

lean_lib ErdosMatching where
  srcDir := "candidates/open-conjectures/erdos-matching"
  roots := #[`Statement]

lean_lib SensitivityConjectureTight where
  srcDir := "candidates/open-conjectures/sensitivity-conjecture-tight"
  roots := #[`Statement]

lean_lib EquationalTheoriesSamples where
  srcDir := "candidates/open-conjectures/equational-theories-samples"
  roots := #[`Statement]