Viewing profile — 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 transl…

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