Formalizing Geometric Algebra (GA) into the language of a theorem prover has the potential to significantly facilitate GA-based reasoning in research, software development, and education, unleashing its power to simplify and unify mathematics involving geometric representation and manipulation. To that end, the formalization should have flexible abstraction levels accessible to common GA practitioners, providing support for both theory development and practical applications to science and engineering. Existing work has certain shortcomings and difficulties in this regard. To achieve the aforementioned flexibility, we present an ongoing GA formalization in Lean, a language supporting the paradigms of theorem proving, functional programming, and meta-programming. This renders it capable of specifying domain-specific objects and rules, verifying their correctness by formally stating and proving theorems, developing proof-building tactics, and integrating with other tools. We choose Lean also for the expressiveness it derives from dependent type theory, the rich library of mathematical components in its Mathematical Library (“mathlib”), and the evolving ecosystem backed by Lean's diverse community of mathematicians and computer scientists. The formalization chooses an axiomatic approach with an emphasis on properties and behaviors rather than representations, ensuring its generality and its compatibility with different styles of mathematical definitions and computational data structures. This approach is naturally coordinate-free, and can support arbitrary (including degenerate) metrics. We demonstrate the elegance and readability in the definitions, the statements and proofs of propositions and identities, as well as the friendly interactive and semi-automatic proving experience, even for readers who have no prior exposure to formalization. This demonstration and the discussions on potential applications and future work establish a good foundation for turning this adventure into a continuous joint effort by the GA community.