University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Formalizing mathematics today

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Formalizing mathematics today

Download to your calendar using vCal

If you have a question about this talk, please contact nobody.

OOEW11 - AI for Maths and Open Science

Formalization of mathematics is the process of translating it from human language into the language of a computer proof assistant such as Lean. Ten years ago it was mostly computer scientists doing it, but now both mathematicians and machines have joined in. I will talk about the following questions. What is the point of doing it? Should humans or computers be doing it (related question: is it a science, or an art)? What are the pain points? And what does the future hold?

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Seminar Room SG2, Alison Richard Building, 7 West Road, Cambridge, CB3 9DT Dyson Seminar Room, Department of Engineering / Online (Zoom Meeting ID: 825 7950 4541 Passcode: 123551) Occasional Talks in Biochemistry

Other talks

title abstract tbc How bubble acoustics can help in three apocalypses Machine Learning for Spectral Geometry and Vice Versa TBC Precarity and the economy of makeshifts: A novel argument from the census of England, 1851-1911 Group Work
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity