4 ms·
Out of curiosity, does anyone know the mathematicians actively leaning into AI + Lean?
by vonnik 11mo ago
Out of curiosity, does anyone know the mathematicians actively leaning into AI + Lean?
- thechao 11mo agoTerence Tao posts on mathstodon fairly regularly about lean, AI, and math. I'm not going to interpret his posts.
- oersted 11mo agoTerence Tao is well known for being enthusiastic about Lean and AI and he regularly posts about his experiments. He is also a serious research mathematician at the top of his game, considered by many one of the best mathematicians alive. This might be biased by the fact that he is such a good communicator, he is more visible than other similarly good mathematicians, but he is a Fields medallist all the same.
- griffzhowl 11mo agoKevin 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
- kronicum2025 11mo agoI'm leaning a lot into AI + lean. It's a fantastic tool to find new proofs. The extremly rigid nature of lean means you can really check programs for correctness. So that part of AI is solved. The only thing that remains is generating proofs, and that is where there's nothing in AI space right now. As soon as we do get something, our mathematical knowledge is going to explode.