Metamath Zero dissertation defense

[Mario Carneiro]

My dissertation defense on Metamath Zero will be held 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: Mon, Jun 13 2022, 1:00 PM (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

[Mario Carneiro]

To clarify, that is Mon, Jun 13 2022, 1:00 PM EDT

[Jon P]

Hey Mario, I've been enjoying your thesis and just wanted to wish you luck with your defence today :)

[heiph...@wilsonb.com]

Congrats, Mario, on making it through a Ph.D. thesis defense! Hope you
destroyed the grilling. I would love to have attended, but it was in the middle
of the night in my time zone. Will a recording be available as well?

[Mario Carneiro]

Thanks everyone for the well wishes. Everything went well and I'm a doctor now. The slides for the talk are up at https://digama0.github.io/mm0/thesis-slides.pdf , and I might record a version of the talk for youtube at some point.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/62a83700.1c69fb81.8e039.badbSMTPIN_ADDED_BROKEN%40gmr-mx.google.com.

[Thierry Arnoux]

Congratulations Mario!

I would also have liked to attend, but the timing was very bad for me (1AM in my timezone) and I'm a bit busy currently.

I'd like to ask "What is your next step now?", but I guess this is already answered somewhere in the slides, towards the end!

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuvcz7ubMAAhwhN-WKLL%2BwgoTZQqMcSqy3dESy-uw3jNA%40mail.gmail.com.

[Antony Bartlett]

Mario writes:

> Everything went well and I'm a doctor now.

Congrats Doc!

heiphohmia writes:

> Hope you destroyed the grilling

I assume this is a phrase of encouragement along the same lines as "knock 'em dead", and that a thesis defence is more like a job interview where the people asking the somewhat adversarial questions are the same ones making the all important decision, such that the best strategy is usually to say something complimentary about the question before answering it?

    Best regards,

        Antony

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3004db09-176b-1dad-17ab-94da17988679%40gmx.net.

[David A. Wheeler]

Sorry I didn't say this earlier, but a HUGE congrats to you for an honor well-deserved.

I wish the very best to you, Dr. Carneiro!

--- David A. Wheeler

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSuvcz7ubMAAhwhN-WKLL%2BwgoTZQqMcSqy3dESy-uw3jNA%40mail.gmail.com.

[OlivierBinda]

O.O

Given the ground breaking amazing work you had been  doing for years.

I'm just surprised you weren't a doctor yet.
I definitely assumed you were.

I mean, you work,your knowledge and your achievement s are not on the
"student" level, but on the "shining star & hope of the mathematical
community" level.

But well, I believe that metamath and mm0 are understated jewels so I'm
biaised.

Congrats,
Looking forward for your next works, always.

Olivier