Repository navigation
Expand file tree
/
Copy pathMiniF2F.lean
More file actions
244 lines (244 loc) · 9.62 KB
/
Copy pathMiniF2F.lean
File metadata and controls
244 lines (244 loc) · 9.62 KB
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
import MiniF2F.Test.aime_1983_p1
import MiniF2F.Test.aime_1983_p2
import MiniF2F.Test.aime_1983_p3
import MiniF2F.Test.aime_1984_p1
import MiniF2F.Test.aime_1984_p7
import MiniF2F.Test.aime_1987_p5
import MiniF2F.Test.aime_1988_p8
import MiniF2F.Test.aime_1989_p8
import MiniF2F.Test.aime_1990_p15
import MiniF2F.Test.aime_1990_p4
import MiniF2F.Test.aime_1991_p9
import MiniF2F.Test.aime_1994_p3
import MiniF2F.Test.aime_1995_p7
import MiniF2F.Test.aime_1997_p9
import MiniF2F.Test.aime_1999_p11
import MiniF2F.Test.algebra_2varlineareq_fp3zeq11_3tfm1m5zeqn68_feqn10_zeq7
import MiniF2F.Test.algebra_9onxpypzleqsum2onxpy
import MiniF2F.Test.algebra_abpbcpcageq3_sumaonsqrtapbgeq3onsqrt2
import MiniF2F.Test.algebra_absapbon1pabsapbleqsumabsaon1pabsa
import MiniF2F.Test.algebra_absxm1pabsxpabsxp1eqxp2_0leqxleq1
import MiniF2F.Test.algebra_amgm_sum1toneqn_prod1tonleq1
import MiniF2F.Test.algebra_amgm_sumasqdivbgeqsuma
import MiniF2F.Test.algebra_apbmpcneq0_aeq0anbeq0anceq0
import MiniF2F.Test.algebra_apbon2pownleqapownpbpowon2
import MiniF2F.Test.algebra_apbpceq2_abpbcpcaeq1_aleq1on3anbleq1ancleq4on3
import MiniF2F.Test.algebra_bleqa_apbon2msqrtableqambsqon8b
import MiniF2F.Test.algebra_cubrtrp1oncubrtreq3_rcubp1onrcubeq5778
import MiniF2F.Test.algebra_ineq_nto1onlt2m1on
import MiniF2F.Test.algebra_others_exirrpowirrrat
import MiniF2F.Test.algebra_sqineq_at2malt1
import MiniF2F.Test.algebra_sqineq_unitcircatbpabsamblt1
import MiniF2F.Test.algebra_sqineq_unitcircatbpamblt1
import MiniF2F.Test.algebra_sum1onsqrt2to1onsqrt10000lt198
import MiniF2F.Test.amc12_2000_p1
import MiniF2F.Test.amc12_2000_p12
import MiniF2F.Test.amc12_2000_p20
import MiniF2F.Test.amc12_2000_p6
import MiniF2F.Test.amc12_2001_p21
import MiniF2F.Test.amc12_2001_p5
import MiniF2F.Test.amc12a_2002_p13
import MiniF2F.Test.amc12a_2002_p6
import MiniF2F.Test.amc12a_2003_p23
import MiniF2F.Test.amc12a_2003_p5
import MiniF2F.Test.amc12a_2008_p25
import MiniF2F.Test.amc12a_2009_p6
import MiniF2F.Test.amc12a_2009_p7
import MiniF2F.Test.amc12a_2013_p4
import MiniF2F.Test.amc12a_2019_p12
import MiniF2F.Test.amc12a_2020_p10
import MiniF2F.Test.amc12a_2020_p15
import MiniF2F.Test.amc12a_2020_p25
import MiniF2F.Test.amc12a_2020_p4
import MiniF2F.Test.amc12a_2020_p7
import MiniF2F.Test.amc12a_2020_p9
import MiniF2F.Test.amc12a_2021_p12
import MiniF2F.Test.amc12a_2021_p14
import MiniF2F.Test.amc12a_2021_p18
import MiniF2F.Test.amc12a_2021_p19
import MiniF2F.Test.amc12a_2021_p22
import MiniF2F.Test.amc12a_2021_p25
import MiniF2F.Test.amc12a_2021_p3
import MiniF2F.Test.amc12a_2021_p8
import MiniF2F.Test.amc12a_2021_p9
import MiniF2F.Test.amc12b_2002_p19
import MiniF2F.Test.amc12b_2002_p2
import MiniF2F.Test.amc12b_2002_p4
import MiniF2F.Test.amc12b_2002_p7
import MiniF2F.Test.amc12b_2020_p13
import MiniF2F.Test.amc12b_2020_p2
import MiniF2F.Test.amc12b_2020_p21
import MiniF2F.Test.amc12b_2020_p22
import MiniF2F.Test.amc12b_2020_p6
import MiniF2F.Test.amc12b_2021_p1
import MiniF2F.Test.amc12b_2021_p13
import MiniF2F.Test.amc12b_2021_p18
import MiniF2F.Test.amc12b_2021_p3
import MiniF2F.Test.amc12b_2021_p4
import MiniF2F.Test.amc12b_2021_p9
import MiniF2F.Test.imo_1959_p1
import MiniF2F.Test.imo_1960_p2
import MiniF2F.Test.imo_1962_p2
import MiniF2F.Test.imo_1963_p5
import MiniF2F.Test.imo_1964_p2
import MiniF2F.Test.imo_1965_p2
import MiniF2F.Test.imo_1968_p5_1
import MiniF2F.Test.imo_1969_p2
import MiniF2F.Test.imo_1974_p3
import MiniF2F.Test.imo_1977_p6
import MiniF2F.Test.imo_1981_p6
import MiniF2F.Test.imo_1982_p1
import MiniF2F.Test.imo_1983_p6
import MiniF2F.Test.imo_1984_p6
import MiniF2F.Test.imo_1985_p6
import MiniF2F.Test.imo_1992_p1
import MiniF2F.Test.imo_1997_p5
import MiniF2F.Test.imo_2001_p6
import MiniF2F.Test.imo_2019_p1
import MiniF2F.Test.imosl_2007_algebra_p6
import MiniF2F.Test.induction_11div10tonmn1ton
import MiniF2F.Test.induction_12dvd4expnp1p20
import MiniF2F.Test.induction_1pxpownlt1pnx
import MiniF2F.Test.induction_nfactltnexpnm1ngt3
import MiniF2F.Test.induction_pord1p1on2powklt5on2
import MiniF2F.Test.induction_pprime_pdvdapowpma
import MiniF2F.Test.induction_prod1p1onk3le3m1onn
import MiniF2F.Test.induction_sumkexp3eqsumksq
import MiniF2F.Test.mathd_algebra_107
import MiniF2F.Test.mathd_algebra_113
import MiniF2F.Test.mathd_algebra_114
import MiniF2F.Test.mathd_algebra_125
import MiniF2F.Test.mathd_algebra_129
import MiniF2F.Test.mathd_algebra_137
import MiniF2F.Test.mathd_algebra_139
import MiniF2F.Test.mathd_algebra_141
import MiniF2F.Test.mathd_algebra_142
import MiniF2F.Test.mathd_algebra_143
import MiniF2F.Test.mathd_algebra_148
import MiniF2F.Test.mathd_algebra_153
import MiniF2F.Test.mathd_algebra_156
import MiniF2F.Test.mathd_algebra_158
import MiniF2F.Test.mathd_algebra_160
import MiniF2F.Test.mathd_algebra_17
import MiniF2F.Test.mathd_algebra_170
import MiniF2F.Test.mathd_algebra_171
import MiniF2F.Test.mathd_algebra_176
import MiniF2F.Test.mathd_algebra_184
import MiniF2F.Test.mathd_algebra_188
import MiniF2F.Test.mathd_algebra_196
import MiniF2F.Test.mathd_algebra_208
import MiniF2F.Test.mathd_algebra_209
import MiniF2F.Test.mathd_algebra_215
import MiniF2F.Test.mathd_algebra_24
import MiniF2F.Test.mathd_algebra_246
import MiniF2F.Test.mathd_algebra_263
import MiniF2F.Test.mathd_algebra_270
import MiniF2F.Test.mathd_algebra_275
import MiniF2F.Test.mathd_algebra_276
import MiniF2F.Test.mathd_algebra_288
import MiniF2F.Test.mathd_algebra_289
import MiniF2F.Test.mathd_algebra_293
import MiniF2F.Test.mathd_algebra_296
import MiniF2F.Test.mathd_algebra_302
import MiniF2F.Test.mathd_algebra_304
import MiniF2F.Test.mathd_algebra_313
import MiniF2F.Test.mathd_algebra_314
import MiniF2F.Test.mathd_algebra_320
import MiniF2F.Test.mathd_algebra_329
import MiniF2F.Test.mathd_algebra_33
import MiniF2F.Test.mathd_algebra_332
import MiniF2F.Test.mathd_algebra_338
import MiniF2F.Test.mathd_algebra_342
import MiniF2F.Test.mathd_algebra_346
import MiniF2F.Test.mathd_algebra_354
import MiniF2F.Test.mathd_algebra_359
import MiniF2F.Test.mathd_algebra_362
import MiniF2F.Test.mathd_algebra_388
import MiniF2F.Test.mathd_algebra_392
import MiniF2F.Test.mathd_algebra_398
import MiniF2F.Test.mathd_algebra_400
import MiniF2F.Test.mathd_algebra_412
import MiniF2F.Test.mathd_algebra_419
import MiniF2F.Test.mathd_algebra_427
import MiniF2F.Test.mathd_algebra_432
import MiniF2F.Test.mathd_algebra_44
import MiniF2F.Test.mathd_algebra_440
import MiniF2F.Test.mathd_algebra_441
import MiniF2F.Test.mathd_algebra_452
import MiniF2F.Test.mathd_algebra_459
import MiniF2F.Test.mathd_algebra_478
import MiniF2F.Test.mathd_algebra_484
import MiniF2F.Test.mathd_algebra_487
import MiniF2F.Test.mathd_algebra_513
import MiniF2F.Test.mathd_algebra_598
import MiniF2F.Test.mathd_algebra_756
import MiniF2F.Test.mathd_algebra_76
import MiniF2F.Test.mathd_algebra_80
import MiniF2F.Test.mathd_numbertheory_100
import MiniF2F.Test.mathd_numbertheory_1124
import MiniF2F.Test.mathd_numbertheory_12
import MiniF2F.Test.mathd_numbertheory_127
import MiniF2F.Test.mathd_numbertheory_135
import MiniF2F.Test.mathd_numbertheory_150
import MiniF2F.Test.mathd_numbertheory_175
import MiniF2F.Test.mathd_numbertheory_185
import MiniF2F.Test.mathd_numbertheory_207
import MiniF2F.Test.mathd_numbertheory_212
import MiniF2F.Test.mathd_numbertheory_222
import MiniF2F.Test.mathd_numbertheory_227
import MiniF2F.Test.mathd_numbertheory_229
import MiniF2F.Test.mathd_numbertheory_233
import MiniF2F.Test.mathd_numbertheory_234
import MiniF2F.Test.mathd_numbertheory_235
import MiniF2F.Test.mathd_numbertheory_237
import MiniF2F.Test.mathd_numbertheory_239
import MiniF2F.Test.mathd_numbertheory_247
import MiniF2F.Test.mathd_numbertheory_254
import MiniF2F.Test.mathd_numbertheory_277
import MiniF2F.Test.mathd_numbertheory_293
import MiniF2F.Test.mathd_numbertheory_296
import MiniF2F.Test.mathd_numbertheory_299
import MiniF2F.Test.mathd_numbertheory_3
import MiniF2F.Test.mathd_numbertheory_314
import MiniF2F.Test.mathd_numbertheory_320
import MiniF2F.Test.mathd_numbertheory_321
import MiniF2F.Test.mathd_numbertheory_328
import MiniF2F.Test.mathd_numbertheory_34
import MiniF2F.Test.mathd_numbertheory_341
import MiniF2F.Test.mathd_numbertheory_342
import MiniF2F.Test.mathd_numbertheory_343
import MiniF2F.Test.mathd_numbertheory_345
import MiniF2F.Test.mathd_numbertheory_353
import MiniF2F.Test.mathd_numbertheory_427
import MiniF2F.Test.mathd_numbertheory_430
import MiniF2F.Test.mathd_numbertheory_435
import MiniF2F.Test.mathd_numbertheory_447
import MiniF2F.Test.mathd_numbertheory_451
import MiniF2F.Test.mathd_numbertheory_457
import MiniF2F.Test.mathd_numbertheory_483
import MiniF2F.Test.mathd_numbertheory_495
import MiniF2F.Test.mathd_numbertheory_5
import MiniF2F.Test.mathd_numbertheory_517
import MiniF2F.Test.mathd_numbertheory_521
import MiniF2F.Test.mathd_numbertheory_541
import MiniF2F.Test.mathd_numbertheory_551
import MiniF2F.Test.mathd_numbertheory_552
import MiniF2F.Test.mathd_numbertheory_559
import MiniF2F.Test.mathd_numbertheory_582
import MiniF2F.Test.mathd_numbertheory_618
import MiniF2F.Test.mathd_numbertheory_66
import MiniF2F.Test.mathd_numbertheory_711
import MiniF2F.Test.mathd_numbertheory_728
import MiniF2F.Test.mathd_numbertheory_764
import MiniF2F.Test.mathd_numbertheory_765
import MiniF2F.Test.mathd_numbertheory_769
import MiniF2F.Test.mathd_numbertheory_85
import MiniF2F.Test.mathd_numbertheory_99
import MiniF2F.Test.numbertheory_2pownm1prime_nprime
import MiniF2F.Test.numbertheory_3pow2pownm1mod2pownp3eq2pownp2
import MiniF2F.Test.numbertheory_4x3m7y3neq2003
import MiniF2F.Test.numbertheory_aoddbdiv4asqpbsqmod8eq1
import MiniF2F.Test.numbertheory_exk2powkeqapb2mulbpa2_aeq1
import MiniF2F.Test.numbertheory_fxeq4powxp6powxp9powx_f2powmdvdf2pown
import MiniF2F.Test.numbertheory_notequiv2i2jasqbsqdiv8
import MiniF2F.Test.numbertheory_x5neqy2p4