Metamath Zero dissertation defense

Skip to first unread message

Mario Carneiro

Jun 7, 2022, 11:46:11 PMJun 7
to metamath

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

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:


Mario Carneiro

Jun 7, 2022, 11:49:28 PMJun 7
to metamath
To clarify, that is Mon, Jun 13 2022, 1:00 PM EDT

Jon P

Jun 13, 2022, 5:58:52 AMJun 13
to Metamath
Hey Mario, I've been enjoying your thesis and just wanted to wish you luck with your defence today :)

Jun 14, 2022, 3:21:37 AMJun 14
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

Jun 14, 2022, 6:55:33 AMJun 14
to metamath
Thanks everyone for the well wishes. Everything went well and I'm a doctor now. The slides for the talk are up at , 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
To view this discussion on the web visit

Thierry Arnoux

Jun 14, 2022, 7:04:14 AMJun 14
to, Mario Carneiro

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!

Antony Bartlett

Jun 14, 2022, 8:23:10 AMJun 14
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,


David A. Wheeler

Jul 17, 2022, 11:50:04 AMJul 17
to Metamath Mailing List
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


Jul 17, 2022, 4:47:47 PMJul 17

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

Looking forward for your next works, always.

Reply all
Reply to author
0 new messages