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 sceptica

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 https://www.youtube.com/watch?v=K5w7VS2sxD0