BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Equational theories project: metatheorems and how to formalise the
 m - Hernán Ibarra Mejia\, THG and Anand Rao Tadipatri\, University of Cam
 bridge
DTSTART:20241031T170000Z
DTEND:20241031T180000Z
UID:TALK222781@talks.cam.ac.uk
CONTACT:Jonas Bayer
DESCRIPTION:In late September this year\, mathematician Terence Tao launch
 ed the equational theories project (https://teorth.github.io/equational_th
 eories/) with the purpose of mapping out the space of equational theories 
 of magmas\; the broader objective of the project is also to experiment wit
 h a paradigm of large-scale collaborative mathematical research where resu
 lts are proved with a combination of human contribution and automated tool
 s\, 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 b
 road class of anti-implications between magma laws using meta-theorems and
  the techniques that were used to formalize these proofs.\n\nRecording: ht
 tps://www.youtube.com/watch?v=wKpl771bav8\n\n=== Hybrid talk ===
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR