nnarek

3 ms·

1. 1.▲
   by nnarek 2y ago

   yes it is very impressive, especially autoformalization of problems written in natural language and also proof search of theorems
2. 2.▲
   by nnarek 2y ago

   formal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it
3. 3.▲
   by nnarek 2y ago

   "three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)