Build a reliable math library [2025mathsig]

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