University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > Equational theories project: metatheorems and how to formalise them

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

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

ℹ️ Information

Equational theories project: metatheorems and how to formalise them

Download to your calendar using vCal

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

In late September this year, mathematician Terence Tao launched the equational theories project (https://teorth.github.io/equational_theories/) with the purpose of mapping out the space of equational theories of magmas; the broader objective of the project is also to experiment with a paradigm of large-scale collaborative mathematical research where results are proved with a combination of human contribution and automated tools, all formally verified using a proof assistant. The project is slightly over four weeks in and 99.9991% complete, with only 20 open conjectures remaining. This talk is about an approach used in the project to prove a broad class of anti-implications between magma laws using meta-theorems and the techniques that were used to formalize these proofs.

Recording: https://www.youtube.com/watch?v=wKpl771bav8

=== Hybrid talk ===

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Churchill College, University of Cambridge Average on weekdays: 8930.00454545 kWh Riley Auditorium, Clare College Memorial Court, Queens Road

Other talks

Title to be confirmed What Can a Spectrum Learn? AI Perspectives on the Kohn Laplacian of Sphere Quotients Title to be confirmed The Imagined Conflict: On Science and God Security Cooperation within Government and between Governments Group Work
 

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