Formalizing invisible mathematics
- 13 February 2023
- Talks
I am at the Machine assisted proofs workshop at the UCLA Institute for Pure and Applied Mathematics, where I am about to give a talk on “Formalizing invisible mathematics”.
Here are the slides with speaker notes and the video recording of the talk.
→ continue readingExploring strange new worlds of mathematics
- 10 February 2023
- Talks, Constructive math
On February 10, 2023, I gave my Levi L. Conant Lectur Series talk “Exploring strange new worlds of mathematics”, at the math department of Worcester Polytechnic Institute. Here are the slides with speaker notes and the video recording of the talk.
→ continue readingHappy birthday, Dana!
- 11 October 2022
- News
Today Dana Scott is celebrating the 90th birthday today. Happy birthday, Dana! I am forever grateful for your kindness and the knowledge that I received from you. I hope to pass at least a part of it onto my students.
On the occasion Steve Awodey assembled selected works by Dana Scott at CMU-HoTT/scott
repository. It is an amazing collection of papers that had deep impact on logic, set theory, computation, and programming languages. I hope in the future we can extend it and possibly present it in better format.
As a special treat, I recount here the story the invention of the famous $D_\infty$ model of the untyped $\lambda$-calculus. I heard it first when I was Dana's student. In 2008 I asked Dana to recount it in the form of a short interview.
→ continue reading (1 comment)One syntax to rule them all
- 20 May 2022
- Talks
I am at the Syntax and Semantics of Type Theory workshop in Stockholm, a kickoff meeting for WG6 of the EuroProofNet COST network, where I am giving a talk “One syntax to rule them all” based on joint work with Danel Ahman.
→ continue readingTwo new doctors!
- 12 January 2022
- News
Within a month two of my students defended their theses: Dr. Anja Petković Komel just before Christmas, and Dr. Philipp Haselwarter just yesterday. I am very proud of them. Congratulations!
→ continue readingIs every projective setoid isomorphic to a type?
- 12 January 2022
- Constructive math, Type theory, Formalization
Jacques Carette asked on Twitter for a refence to the fact that countable choice holds in setoids. I then spent a day formalizing facts about the axiom of choice in setoids in Agda. I noticed something interesting that is worth blogging about.
→ continue reading (4 comments)The proposal for a proof assistants StackExchange site
- 20 November 2021
- General, Proof assistant
Proof assistant communities have grown quite a bit lately. They have active Zulip chats: Lean, Coq, Agda, Isabelle. These are good for discussions, but less so for knowledge accumulation and organization, and are not indexed by the search engines.
I have therefore created a proposal for a new “Proof assistants” StackExchange site. I believe that such a site would complement very well various Zulips dedicated to specific proof assistants. If you favor the idea, please support it by visiting the proposal and
- becoming a follower (you have to be a registered user with a verified email account),
- asking sample questions, and
- upvoting good sample questions.
To pass the first stage, we need 60 followers and 40 questions with at least 10 votes to proceed to the next stage.
→ continue reading (2 comments)The dawn of formalized mathematics
- 24 June 2021
- Talks, Formalization
Here are the slides of my talk "The dawn of formalized mathematics" from the 8th European Congress of Mathematics, which is taking place online and in Protorož, Slovenia, from June 20 to 26, 2021:
- Keynote presentation, viewable online in your browser. Turn on the speaker notes by clicking on the rectangular icon in the top-left corner.
- Slides with speaker notes (PDF). Unfortunately, Keynote does not make the hyperlinks active when exporting PDF.
- Video recording of the talk.
Computing an integer using a Grothendieck topos
- 18 May 2021
- Constructive math, Type theory, Formalization
A while ago, my former student Chuangjie Xu and I computed an integer using a sheaf topos. For that purpose,
- we developed our mathematics constructively,
- we formalized our mathematics in Martin-Löf type theory, in Agda notation,
- we pressed a button, and
- after a few seconds we saw the integer we expected in front of us.
Well, it was a few seconds for the computer in steps (3)-(4), but three years for us in steps (1)-(2).
→ continue readingThe Burali-Forti argument in HoTT/UF
- 22 February 2021
- Type theory, Constructive math
This is joint work with Marc Bezem, Thierry Coquand, Peter Dybjer.
We use the Burali-Forti argument to show that, in homotopy type theory and univalent foundations, the embedding $$ \mathcal{U} \to \mathcal{U}^+$$ of a universe $\mathcal{U}$ into its successor $\mathcal{U}^+$ is not an equivalence. We also establish this for the types of sets, magmas, monoids and groups. The arguments in this post are also written in Agda.
→ continue reading