FormalMATH: A Large-Scale Benchmark for Formal Mathematical Reasoning in Lean4