Lean 4 is a proof assistant, that is, a software that can be used to encode mathematical statements and proofs, and teach them to a computer. If the program compiles, then the proof is correct and completely verified. I will start this talk by a general presentation on Lean 4 and its large mathematical library Mathlib. I will then discuss the state of the art in Spectral Geometry, and the impact of AI in the formalisation of mathematics.