nnarek
No user record in our sample, but nnarek has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
No user record in our sample, but nnarek has activity below (stories or comments). Likely we have partial data — the full bulk-load will fill profiles in.
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…
"three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)