According to AIBASE, the OpenBMB team has formally made MathForm available as open-source software. This automatic mathematical formalization framework encompasses a dataset and model, specifically designed to tackle the challenge of generating code that, while compilable, may suffer from semantic inaccuracies within the realm of mathematical formalization. The framework incorporates a retrieval-augmented and verification-guided data construction approach. By leveraging a retrieval planner to extract definitions from Mathlib, the generator refines its output by integrating diagnostic feedback from the Lean compiler with insights on semantic consistency. The dataset, named FormalVerse, boasts a collection of over 367,000 verified Lean4 examples. Experimental results indicate that the model trained on this dataset attains a consistency check rate of 60.32%. The central model, MathForm-8B, demonstrates an impressive 88.06% pass rate in syntax checks and a 72.37% pass rate in consistency checks across six benchmark tests.