search

albertqjiang / miniF2F

An updated version of miniF2F with problems fixed
0 stars 0 forks source link

[Lean Fix] imo_1974_p3 & amc12b_2021_p4 #32

Closed DyeKuu closed 2 years ago

DyeKuu commented 2 years ago

Note:

For imo_1974_p3, the sum is inclusive of n. When n = 0, the previous lean version doesn't carry out the computation. @Wenda302 will that make the statement correct if n = 0, the sum still has 1 element (resulting in ~(5|1) and that looks correct)?

Adding proof to amc12b_2021_p4, looks good in lean version.

Wenda302 commented 2 years ago

imo_1974_p3 is correct when n=0 in Isabelle :-)

DyeKuu commented 2 years ago

good, let's merge this one.