Content
@
0 reply
0 recast
0 reaction
Agost Biro
@agostbiro
Prof Kevin Buzzard gave a talk[1] at Microsoft in 2019 how he got started with Lean as a teaching tool for undergrads and how he intends to transform modern mathematics by formalizing it with Lean. There has been a lot of progress in that and he has now a research grant to formalize the proof of Fermat's Last Theorem with Lean.[2] What was not foreseen at the time of his 2019 talk is that AI researches have adopted Lean for models that generate proofs.[3] [1] https://www.youtube.com/watch?v=Dp-mQ3HxgDE [2] https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/ [3] https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/
1 reply
0 recast
5 reactions
