Metamath Zero thesis defense

Stream: general

[Mario Carneiro]

My dissertation defense is next week! It's open to the public.

Please join us for the Final Public Oral Examination for the degree, Doctor of Philosophy in Pure and Applied Logic

Mario Carneiro

Title: Metamath Zero: From Logic, to Proof Assistant, to Verified Compiler

Committee:
Jeremy Avigad, Carnegie Mellon University, chair
Thomas Hales, University of Pittsburgh
Wilfried Sieg, Carnegie Mellon University
John Harrison, Amazon Web Services

Date & time: 2022-06-13T13:00:00-04:00 (45 minutes talk + questions)
Location: (Baker Hall 150 or) Zoom:
https://cmu.zoom.us/j/98691564266?pwd=R0ZSSk9qSS9QY3N5WnRLakJWcDJ4UT09

Thesis: https://digama0.github.io/mm0/thesis.pdf

[Patrick Massot]

Great! It feels like this went faster than your MS Thesis, but maybe it's only me getting older and loosing track of time.

[Mario Carneiro]

it's about 2.5 years in the making

[Mario Carneiro]

the project itself isn't going to end here either, it's just going to go back to a hobby project, maybe with the occasional paper

[Patrick Massot]

Do you know what will be your main occupation if MM0 becomes a hobby?

[Mario Carneiro]

Lean related stuff probably

[Mario Carneiro]

or possibly other formal verification jobs if the lean opportunities dry up

[Patrick Massot]

To you plan to devote more time to mathport after defending your thesis?

[Mario Carneiro]

Maybe? It seems like one of the more likely work items

[Mario Carneiro]

Reminder: Mario's thesis defense, 2022-06-13T13:00:00-04:00, Zoom link, Thesis

[Chris Bailey]

glhf

[Patrick Thomas]

Will it be recorded?

[Mario Carneiro]

Sorry, it wasn't (I asked). I might record a private version for youtube at some point. Slides: https://digama0.github.io/mm0/thesis-slides.pdf . In any case, I'm a doctor now :tada:

[Oliver Nash]

Boom, congrats!

[Patrick Thomas]

No problem, I got to see it. Congratulations!