Talk at "Big proof"

Stream: Equational

[Terence Tao]

I'll be giving a talk tomorrow, mostly on the ETP, at the "Big Proof" event in Cambridge. Unfortunately I could not attend in person and am giving the talk virtually (which was somewhat inconvenient due to time zones). I have uploaded the slides here, am happy to receive any feedback.

I am currently overextended on several other obligations, but I do plan to get back to the paper writing tasks to wrap up the primary portion of the project at some point in the near future.

[Bruno Le Floch]

If you have time, please update the author list to the latest version from https://github.com/teorth/equational_theories/blob/main/paper/main.tex plus Marco Petracci who has an approved but unmerged pull request github.com/teorth/equational_theories#1230 namely

Matthew Bolan, Joachim Breitner, Jose Brox, Mario Carneiro,
Martin Dvo\v{r}\'ak, Andr\'es Goens, Aaron Hill,
Harald Husum, Zoltan Kocsis, Bruno Le Floch, Lorenzo Luccioli,
Alex Meiburg, Pietro Monticone, Giovanni Paolini, Marco Petracci,
Bernhard Reinke, David Renshaw, Marcus Rossel, Cody Roux,
J\'er\'emy Scanvic, Shreyas Srinivas, Anand Rao Tadipatri,
Terence Tao, Vlad Tsyrklevich, Daniel Weber, Fan Zheng

Unrelated typos:

• on page 14 of the pdf the figure is too wide
• p19 and p20 the number 4692 should be 4694: if you want to exclude Law 1 and 2 the number of potential edges is not the one given.
• p22 In Tarski's axiom (( should be (.
• p36 "devloped an" → "developed a"

[Shreyas Srinivas]

Slide 14 has a bit of overflow on the left and right

[Shreyas Srinivas]

In slide 39 I am not sure what a light weight proof assistant would be

[Shreyas Srinivas]

A lighter proof assistant strikes me as something like metamath that has minimal built in automation and a simple kernel

[Shreyas Srinivas]

What might be useful is the ability to access a CAS solver which produces proof certificates which can be imported to lean.

[Shreyas Srinivas]

These are usually powerful systems, like mathematica or Sagemath. They are not very lightweight, and usually they don’t produce proofs of correctness of their assertions