albertqjiang / miniF2F

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

[Lean Metamath Isabelle HOL Light Fix] Mathd algebra 332 & Lean proof #24

Closed DyeKuu closed 2 years ago

DyeKuu commented 2 years ago

Note:

Fixing the statement. @malachaux Thank you for the informal collection! It's really helpful for a glance through the informal statement to fix these formal statements. cc @albertqjiang for the Isabelle fix.