Equational theories project: metatheorems and how to formalise them

Add to your list(s) Download to your calendar using vCal

• Hernán Ibarra Mejia, THG and Anand Rao Tadipatri, University of Cambridge
• Thursday 31 October 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

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:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.