Join us for a workshop on Lean, in Appleton tower room AT.M2 from 17:00 to 19:00 on the 30th of September.
Digitizing mathematics is increasingly becoming more popular within the mathematical community and abroad. From the formalization of the Polynomial Freiman-Rusza conjecture lead by Field medalist Terence Tao, to Deepmind’s AlphaProof attaining a silver medal in the IMO, to Kevin Buzzard’s public project to formalize Fermat’s Last Theorem and all the modern algebraic number theory and algebraic geometry leading up to it, to university classrooms beginning to teach using these systems, to Amazon using these systems to verify software, to countless other applications and use cases.
Who knows what the implications are of digitizing mathematics?
I definitely would not be surprised if Interactive Theorem Provers like Lean revolutionized the way mathematics is verified, done, used and taught in the future.