Kevin Buzzard has been the main mathematician involved with Lean

This is a recent talk where he discusses putting it together with LLMs (he's somewhat sceptical it'll be revolutionary for producing new mathematics any time soon)

https://www.youtube.com/watch?v=K5w7VS2sxD0