albertqjiang / miniF2F

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

[Lean Metamath Isabelle Fix] imo_2019_p1 & Rename HOL Light file #31

Closed DyeKuu closed 2 years ago

DyeKuu commented 2 years ago

Note:

Add a bracket to the first assertion. I didn't check whether the metamath passed the grammar check as I didn't setup the env for it. cc @albertqjiang