Formalised proofs and Lean in particular are still too cumbersome for the ``working'' mathematician to use it day-to-day for research-level math. But clearly there is some interest on where it may take us in future.