How to display a formal data set correctly
yyyhz opened this issue · 1 comments
yyyhz commented
I have already configure LeanDojo.
But I am not familiar with LEAN language, so when I use minif2f dataset, there are some errors like "\u2115" with json.
For example:
{"full_name": "amc12a_2019_p21", "statement": "theorem amc12a_2019_p21 (z : \u2102) (h\u2080 : z = (1 + Complex.I) / Real.sqrt 2) :\n ((\u2211 k : \u2124 in Finset.Icc 1 12, z ^ k ^ 2) * (\u2211 k : \u2124 in Finset.Icc 1 12, 1 / z ^ k ^ 2)) = 36", "url": "https://github.com/wzj423/lean-dojo-mew", "commit": "1ef4e4cac9dd370b7be6d648ce135a06aa6fce5f", "file_path": "MiniF2F/Validation.lean", "split": "valid"}
I wonder how to display it.
objecti0n commented
json.dumps(x, ensure_ascii=False)