Metamath Zero dissertation defense

109 views
Skip to first unread message

Mario Carneiro

unread,
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

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

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

Jon P

unread,
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 :)

heiph...@wilsonb.com

unread,
Jun 14, 2022, 3:21:37 AMJun 14
to meta...@googlegroups.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

unread,
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 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

unread,
Jun 14, 2022, 7:04:14 AMJun 14
to meta...@googlegroups.com, 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

unread,
Jun 14, 2022, 8:23:10 AMJun 14
to meta...@googlegroups.com
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



David A. Wheeler

unread,
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 https://groups.google.com/d/msgid/metamath/CAFXXJSuvcz7ubMAAhwhN-WKLL%2BwgoTZQqMcSqy3dESy-uw3jNA%40mail.gmail.com.

OlivierBinda

unread,
Jul 17, 2022, 4:47:47 PMJul 17
to meta...@googlegroups.com
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
Reply all
Reply to author
Forward
0 new messages