# Posts in the year 2021

### 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 mathematics, 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 reading### The Burali-Forti argument in HoTT/UF

- 22 February 2021
- Type theory, Constructive mathematics

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### Synthetic mathematics with an excursion into computability theory

- 03 February 2021
- Talks, Synthetic computability

It is my pleasure to have the opportunity to speak at the University of Wisconsin Logic seminar. The hosts are graciously keeping the seminar open for everyone. I will speak about a favorite topic of mine:

##### Synthetic mathematics with an excursion into computability theory

**Speaker:** Andrej Bauer (University of Ljubljana)

**Location:** University of Wisconsin Logic seminar

**Time:** February 8th 2021, 21:30 UTC (3:30pm CST in Wisconsin, 22:30 CET in Ljubljana)

**Video link:** the Zoom link is available at the seminar page

**Abstract:**

According to Felix Klein, “synthetic geometry is that which studies figures as such, without recourse to formulae, whereas analytic geometry consistently makes use of such formulae as can be written down after the adoption of an appropriate system of coordinates”. To put it less eloquently, the synthetic method axiomatizes geometry directly by construing points and lines as primitive notions, whereas the analytic method builds a model, the Euclidean plane, from the real numbers.

Do other branches of mathematics posses the synthetic method, too? For instance, what would “synthetic topology” look like? To build spaces out of sets, as topologists usually do, is the analytic way. The synthetic approach must construe spaces as primitive and axiomatize them directly, without any recourse to sets. It cannot introduce continuity as a desirable property of functions, for that would be like identifying straight lines as the non-bending curves.

It is indeed possible to build the synthetic worlds of topology, smooth analysis, measure theory, and computability. In each of them, the basic structure – topological, smooth, measurable, computable – is implicit by virtue of permeating everything, even logic itself. The synthetic worlds demand an economy of thought that the unaccustomed mind finds frustrating at first, but eventually rewards it with new elegance and conceptual clarity. The synthetic method is still fruitfully related to the analytic method by interpretation of the former in models provided by the latter.

We demonstrate the approach by taking a closer look at synthetic computability, whose central axiom states that there are countably many countable subsets of the natural numbers. The axiom is validated and explained by its interpretation in the effective topos, where it corresponds to the familiar fact that the computably enumerable sets may be computably enumerated. Classic theorems of computability may be proved in a straightforward manner, without reference to any notion of computation. We end by showing that in synthetic computability Turing reducibility is expressed in terms of sequential continuity of maps between directed-complete partial orders.

The **slides** and the **video**
recording of the talk are now available.