Build a reliable math library [lean_talk_2025]

I gave a talk on the 6th plenary meeting of NJUPT SAST MathSIG, about Lean 4 and Mathlib.