Ph.D. thesis Pursuit of Truth and Beauty in Lean 4

Stream: general

[Martin Dvořák]

Dear colleagues,

I would like to invite you to my Ph.D. defense, which will take place online on 2026-02-11 at:
2026-02-11T17:00:00+01:00

A draft of my Ph.D. thesis Pursuit of Truth and Beauty in Lean 4 is here:
https://madvorak.github.io/2026_Dvorak_Martin_Thesis_draft.pdf

The text is based on the following four repositories:
https://github.com/madvorak/duality/tree/v3.3.0
https://github.com/madvorak/vcsp/tree/v8.1.0
https://github.com/Ivan-Sergeyev/seymour/tree/v1.1.0
https://github.com/madvorak/chomsky/tree/v1.0.0

What makes my Ph.D. thesis relevant specifically for this community is that the one and only prerequisite for reading it is to know Lean. Everything else is explained through Lean 4.18.0 and plain English, without assuming prior knowledge of any other notation or mathematical background.

Happy new year!

[cmlsharp]

Congratulations!

[Martin Dvořák]

Acknowledgments listed on page 6:

• Vladimir Kolmogorov
• @Jasmin Blanchette
• David Bartl
• Kate Kočická
• @Patrick Johnson
• @Floris van Doorn
• @Damiano Testa
• @Henrik Böving
• @Kevin Buzzard
• @Richard Copley
• @Antoine Chambert-Loir
• @Andrew Yang
• @Emilie (Shad Amethyst)
• @Yaël Dillies
• @Pietro Monticone
• @Riccardo Brasca
• @Johan Commelin
• @Edward van de Meent
• @Aaron Liu
• @Christian Merten
• @Jireh Loreaux

I attempted to be very careful to not forget anybody, yet it might still happen. If you are somebody who helped me with anything that is a part of my Ph.D. thesis but you don't see your name, please, let me know so that I can (1) apologize and (2) acknowledge you in the next version!

[Martin Dvořák]

Do you think there will be any listeners who don't speak Lean?

[Yaël Dillies]

I assume you know the composition of your jury? If all of them speak lean, I would assume the same of the audience

[Martin Dvořák]

Do we have this logo in higher res?
https://www.csee.umbc.edu/wp-content/uploads/sites/659/2023/06/lean_logo2.png

[Michael Rothgang]

Echoing Yael: I would aim my talk at my jury (not the external audience). Usually, that jury includes some non-experts in your subject, so these purposes overlap.

[Martin Dvořák]

Why would there be non-experts among the jury?

[Martin Dvořák]

Michael Sammler
Adam Topaz
Matthew Ballard
Jireh Loreaux
Alex Kontorovich
Terence Tao

They are all experts!

[Mirek Olšák]

Martin Dvořák said:

Do we have this logo in higher res?
https://www.csee.umbc.edu/wp-content/uploads/sites/659/2023/06/lean_logo2.png

This seems slightly higher-res. https://www.microsoft.com/en-us/research/wp-content/uploads/2022/07/LEAN-Theorem-Prover-1024x550.png, but it looks that the logo with THEOREM PROVER is not up-to-date.

[Michael Rothgang]

My jury had a chair (who was not in my area, symplectic geometry). I'm not sure if Michael Sammler is a Lean expert, looks like he knows a lot more Rocq :-)

[Henrik Böving]

Michael has done some Lean, I think that in combination with his Rocq experience will be enough to follow.

[Martin Dvořák]

I'm sure that @Michael Sammler knows more about Lean than I do.

[Martin Dvořák]

I would like to thank @Johannes Tantow for spotting a mistake in my thesis
image.png
and I would like to encourage anybody who finds any mistake to tell me about it.

[Damiano Testa]

Wait, your references are not formally verified?

[Martin Dvořák]

Hopefully one day we will do math with no references, only imports. Now we can only dream of it.

[Martin Dvořák]

On second thought, though, I think I will always want to give credit to the OGs, even if my entire publication is a Lean project without any "text".

[Nick Adfor]

There's even Apple Pen and Pineapple Pen in the paper :)

[David Michael Roberts]

W. Shakespeare, The Tragedy of Hamlet, Prince of Denmark, London: The Folio
Society, 1601

ummm

The Folio Society is an independent London-based publisher, founded by Charles Ede in 1947 and incorporated in 1971

First Folio ≠ The Folio Society.

[David Michael Roberts]

The First Quarto version of Hamlet was published with title page

THE | Tragicall Historie of | HAMLET | Prince of Denmarke | by William Shake-speare. | As it hath beene diuerse times acted by his Highnesse ser- | uants in the Cittie of London : as also in the two V- | niuersities of Cambridge and Oxford, and else-where | At London: printed for N. L. and Iohn Trundell. | 1603. (66 pp.)

cf https://en.wikipedia.org/wiki/List_of_Shakespeare_plays_in_quarto#/media/File:Hamlet_Q1_Frontispiece_1603.jpg

So in modern terms

W. Shakespeare, "The Tragicall Historie of Hamlet, Prince of Denmarke", London, N.L. and John Trundell, 1603.

Writing/performance was indeed sometime 1898-1602, according to Wikipedia, but publication date really should be First Quarto, or else perhaps First Folio.

[David Michael Roberts]

However, I see that the First Quarto of Hamlet is a bad edition, and not the text we know!

[David Michael Roberts]

Also articles by Freiburger–Swaine and Freiburger–Sweine, possibly the same people?

[Martin Dvořák]

Swaine it is. Sweine is a typo. Good catch!

[Martin Dvořák]

David Michael Roberts said:

So in modern terms

W. Shakespeare, "The Tragicall Historie of Hamlet, Prince of Denmarke", London, N.L. and John Trundell, 1603.02, according to Wikipedia, but publication date really should be First Quarto, or else perhaps First Folio.

It isn't https://en.wikipedia.org/wiki/John_Trudell is it?

[David Michael Roberts]

Screenshot 2026-01-28 at 1.14.59 PM.png

I don't know why someone living in the 20th century could be confused for a contemporary of Shakespeare.

[Martin Dvořák]

Fixed. Thanks for all the suggestions!

At the same time, I finally managed to make the bold characters be still bold when inside matrices.

[Chris Anto Fröschl]

I really like what you've written. Thanks for sharing.

Here are some potential problems I noticed: (by pdf page, not page number)

• 21: "reüpload", if not by deliberately for the sake of amusement
• 24, 94 and 72: "reüsable"
• multiple parts: " Moreöver" or "whereäs"
• 145: "we have a learnt a lot about Lean" should probably be "we have learnt a lot about Lean" (i.e. without the double 'a')
• 148: "coïncide", not sure if the double dot character is intended

(There seems to be a general problem with double dot letters (?))

Hope that helps.

[Johannes Tantow]

That is deliberate : https://en.wikipedia.org/wiki/Diaeresis_(diacritic) even if it looks strange for people whose native language includes that as normal letters.

[Martin Dvořák]

Chris Anto Fröschl said:

145: "we have a learnt a lot about Lean" should probably be "we have learnt a lot about Lean" (i.e. without the double 'a')

Ooops! Good catch!

As for the other things, they aren't mistakes — I just like to use the oldschool orthography (which includes diaeresis).

[Martin Dvořák]

Johannes Tantow said:

That is deliberate : https://en.wikipedia.org/wiki/Diaeresis_(diacritic) even if it looks strange for people whose native language includes that as normal letters.

Yeah. Unfortunately, diaeresis almost disappeared because typewriters didn't have these characters. Hopefully, diaeresis seems to be making a slow comeback
ngram_diaeresis.png
but it might be just my wishful thinking...

[Chris Anto Fröschl]

Martin Dvořák said:

the oldschool orthography (which includes diaeresis)

I already expected that this might be some idiom I'm unaware of. Glad to learn something new.

I hope to return more feedback as soon as I finish the whole reading process.

[Philippe Duchon]

Congratulations in advance!

Minor quibble: I found the information (at least a country) by looking at the manuscript, but you might want to complete your announcements with a description of the physical location of your defense - assuming it will not take place purely in cyberspace (I have some rather dreadful memories of Covid-era Ph.D defenses where every participant was in their kitchen/living-room/whatever, and I sincereley hope for you that your defense will take place with at least friends and others physically present).

[Oisin McGuinness]

Small typo in bibliography, the 'Russel' in the citation for Russell and Whitehead (reference [12] currently, see page "136") should be Russell. (I had more for main text, but you fixed those!).

[Martin Dvořák]

Philippe Duchon said:

Minor quibble: I found the information (at least a country) by looking at the manuscript, but you might want to complete your announcements with a description of the physical location of your defense

Heinzel seminar room
Ground Floor of the West Office Building
Am Campus 1
Klosterneuburg
Austria
Europe

[Martin Dvořák]

I have heard that quite a few people who don't know Lean will nevertheless come to my talk, so I'll try to adjust my presentation a bit.

I first thought it wouldn't be the case — for people in Austria, the talk is too late; and for people who will join online, all of them will come from Zulip and everybody speaks Lean here.

[Shreyas Srinivas]

Full disclosure : I only type lean. I don’t speak it xD

[Martin Dvořák]

I'm adding more quotes into my slideshow.

Who is the author of the quote about Lean incentivizing mathematicians to develop more powerful abstractions?

[Ruben Van de Velde]

This? https://www.imo.universite-paris-saclay.fr/~patrick.massot/files/exposition/why_formalize.pdf

[Martin Dvořák]

Oh. I already have quote by Patrick Massot in my slides (and it is from the same article). Maybe somebody else said something similar I could quote?

[Martin Dvořák]

One thing I would like to do to improve my thesis (but won't have enough time to do it throughout, unfortunately) is to replace metatext by text. Ideally, text should be sufficient on its own, and I shouldn't waste readers' time by inserting metatext.
metatext.png
Here, the first line should perhaps say:
"The concatenation of lists is defined by recursion on the left argument:"
Do you agree?

[Michael Rothgang]

My personal opinion:

• "The concatenation of lists is defined by recursion on the left argument" sounds good to me
• Metatext is better than no text! I find documents with just adjacent code blocks and no text/metatext in between quite unreadable. (This is a personal preference. Others prefer terse "definition", "lemma", "proof" writing - or the Lean code equivalent of it.)
• Saying "concept X is defined by recursion" twenty times also feels repetitive. (Even if it's true.) This is something to watch out for.

[Antoine Chambert-Loir]

The idea of removing metatext seems to me similar as removing polite phrases in discourse. They are technically unnecessary but help making the world a bit easier to cope with.

[Jasmin Blanchette]

I disagree that such text is metatext in the first place. To me, metatext is text like "This section explains ...", where the subject or object is the text itself.

[Jasmin Blanchette]

Just using "as follows" doesn't quite qualify for me.

[Jasmin Blanchette]

Regardless, I prefer the thesis as it is.

[Rida Hamadani]

Does anyone have a link for the meeting?

[Ruben Van de Velde]

https://talks-calendar.ista.ac.at/events/6279

[Nick Adfor]

I forgot the time :(

[Nick Adfor]

Any records? :folded_hands:

[Martin Dvořák]

Nah, the talk was not that good to be worth recording.

[J. J. Issai (project started by GRP)]

Will you make a vlog about your defense? I think the experience of a Ph.D. defense will be of interest to many potential Ph.D.s, especially those in the same or adjacent area to your work.

[J. J. Issai (project started by GRP)]

(I would watch it.)