nnarek

yes it is very impressive, especially autoformalization of problems written in natural language and also proof search of theorems

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 is very interesting how they initially formalized problem without including answer in it

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