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)

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

1. A complete ordered field is archimedean.
2. Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in F$ is an upper bound for the natural numbers, construed as a subset of $F$, then so $b - 1$, but then no element of $F$ can be the least upper bound of $\mathbb{N}$. By excluded middle, above every $x \in F$ there is $n \in \mathbb{N}$.

So I asked myself and the constructive news mailing list what the constructive status of the theorem is. But something was amiss, as Fred Richman immediately asked me to provide an example of a complete ordered field. Why would he do that, don't we have the MacNeille reals? After agreeing on definitions, Toby Bartels gave the answer, which I am taking the liberty to adapt a bit and present here. I am probably just reinventing the wheel, so if someone knows an original reference, please provide it in the comments.

The theorem holds constructively, but for a bizarre reason: if there exists a complete ordered field, then the law of excluded middle holds, and the standard proof is valid!

→ continue reading (11 comments)

You may have noticed that lately I have had trouble with the blog. It was dying periodically because the backend database kept crashing. It was high time I moved away from Wordpress anyway, so I bit the bullet and ported the blog.

→ continue reading (4 comments)

Here are the slides with speaker notes for the talk What is an explicit bijection which I gave at the 31st International Conference on Formal Power Series and Algebraic Combinatorics (FPSAC 2019). It was the "outsider" talk, where they invite someone to tell them something outside of their area.

So how does one sell homotopy type theory to people who are interested in combinatorics? That is a tough sell. I used my MathOverflow question "What is an explicit bijection?" to give a stand-up comedy introduction, after which I plunged into type theory. I am told I plunged a little too hard. For instance, people asked "why are we doing this" because I did not make it clear enough that we are trying to make a distinction between "abstractly exists" and "concretely constructed". Oh well, it's difficult to explain homotopy type theory in 50 minutes. Anyhow, I hope you can get something useful from the slides.

Download slides: what-is-an-explicit-bijection.pdf

Video recording of the lecture is now available.

→ continue reading (2 comments)

Here are the slides for the talk I just gave at TYPES 2017 in Budapest. It is joint work with Philipp Haselwarter and Théo Winterhalter. The abstract for the talk is available online.

It describes a complete formalization of dependent type theory which allows you to turn various features of type theory on and off, and it proves several basic formal theorems.

GitHub repository: formal-type-theory
Slides: TYPES 2017  – A modular formalization of type theory in Coq [PDF]

→ continue reading (5 comments)

I have participated in a couple of lengthy discussions about formal proofs. I realized that an old misconception is creeping in. Let me expose it.

→ continue reading (24 comments)

A postdoc position in the Effmath research project is available at the University of Ljubljana, Faculty of Mathematics and Physics. The precise topic is flexible, but should generally be aligned with the project (see project description). Possible topics include:

•  reasoning about computational effects
•  implementation of computational effects
• proof assistants and formalization of mathematics

The candidate should have a PhD degree in mathematics or computer science, with background knowledge relevant to the project area. The position is available for a period of one year with possibility of extension, preferably starting in early 2016. No knowledge of the Slovene language is required.

The candidates should contact Andrej Bauer by email as soon as possible, but no later than January 8th 2016. Please include a short CV and a statement of interest.

→ continue reading

This is officially a rant and should be read as such.

Here is my pet peeve: theoretical computer scientists misuse the word “provably”. Stop it. Stop it!

→ continue reading (10 comments)

It is my pleasure to announce a second PhD position in Ljubljana!

A position is available for a PhD student at the University of Ljubljana in the general research area of modelling and reasoning about computational effects. The precise topic is somewhat flexible, and will be decided in discussion with the student. The PhD will be supervised by Alex Simpson who is Professor of Computer Science at the Faculty of Mathematics and Physics.

The position will be funded by the Effmath project (see project description). Full tuition & stipend will be provided.

The candidate should have a master's (or equivalent) degree in either mathematics or computer science, with background knowledge relevant to the project area. The student will officially enrol in October 2015 at the University of Ljubljana. No knowledge of the Slovene language is required.

The candidates should contact Alex.Simpson@fmf.uni-lj.si by email as soon as possible. Please include a short CV and a statement of interest.

→ continue reading

Recently I reviewed a paper in which most proofs were done in a proof assistant. Yes, the machine guaranteed that the proofs were correct, but I still had to make sure that the authors correctly formulated their definitions and theorems, that the code did not contain hidden assumptions, that there were no unfinished proofs, and so on.

In a typical situation an author submits a paper accompanied with some source code which contains the formalized parts of the work. Sometimes the code is enclosed with the paper, and sometimes it is available for download somewhere. It is easy to ignore the code! The journal finds it difficult to archive the code, the editor naturally focuses on the paper itself, the reviewer trusts the authors and the proof assistant, and the authors are tempted not to mention dirty little secrets about their code. If the proponents of formalized mathematics want to avert a disaster that could destroy their efforts in a single blow, they must adopt a set of rules that will ensure high standards. There is much more to trusting a piece of formalized mathematics than just running it through a proof checker.

→ continue reading (17 comments)

The HoTT book is finished!

Since spring, and even before that, I have participated in a great collaborative effort on writing a book on Homotopy Type Theory. It is finally finished and ready for public consumption. You can get the book freely at http://homotopytypetheory.org/book/. Mike Shulman has written about the contents of the book, so I am not going to repeat that here. Instead, I would like to comment on the socio-technological aspects of making the book, and in particular about what we learned from open-source community about collaborative research.

→ continue reading (10 comments)

It seems to me that people think I am a constructive mathematician, or worse a constructivist (a word which carries a certain amount of philosophical stigma). Let me be perfectly clear: it is not decidable whether I am a constructive mathematician.

→ continue reading (44 comments)

This is an advertisement for two great meetings we are organizing in Ljubljana from June 15 to June 20, 2012:

• Fourth workshop on formal topology (June 15—19)
• Workshop on Higher Dimensional Algebra, Categories and Types (June 20)

There are many reasons why you should come: Ljubljana is lovely in June, with many cafes and restaurants on the Ljubljanica river bank, we have a very interesting programme, and when will you next be able to attend a meeting in which the keynote speakers are Per Martin-Löf, Ieke Moerdijk and Vladimir Voevodsky? Not to mention that the schedule is fairly light, everything is within walking distance, and we are organizing dinners at some excellent restaurants.

If you decide to come, make sure to book a hotel early and register today!

→ continue reading (4 comments)

I remember how hard it was to assimilate category theory when I was a student. A beginning student on math.stackexchange.com is asking for a solution to a basic lemma about pullbacks. It really is the sort of thing one should do by oneself. Nevertheless, here it is, in gory details.

Download: pullback.pdf

→ continue reading (1 comment)

Last year I participated in a project whose goal was to record at low cost my lectures on video and put them on-line. Since the most expensive parts of recording are having a camera man and manual post production, we set up a static camera and just uploaded raw video online at videolectures.net. As you can see for yourself, the sound is good (I wore a microphone) but the whiteboard is mostly illegible. In addition, it took about two weeks for the lectures to show up on-line because there were men-in-the-middle. So that got me thinking whether there was a better way.

→ continue reading (23 comments)

Next week I am going to a meeting where I am supposed to give a tutorial on the Coq proof assistant. Inspired by the Catsters, I decided to prepare the material in the form of screencasts. You can find the first few tutorials on Youtube in my “Coq tutorials” playlist. So far I have:

• Obtaining and installing the Coq proof assistant
• How to use CoqIDE
• How to use Coq with Proof General
• A first proof with Coq (Frobenius rule)
• The dual Frobenius rule, part 1
• The dual Frobenius rule, part 2
• Currying and uncurrying, part 1
• Currying and uncurrying, part 2

You should turn on the high quality HD stream when you watch these. Feedback is welcome (and easy to provide on Youtube). I find it very, very difficult to listen to my own voice. I hope to have many more lectures soon, but I am starting to feel out of my depth, so if anyone wants to help they are welcome!

→ continue reading (17 comments)

[Edit 2010-11-12: Given the gap in my “proof”, I am changing the title of the post to a question.]

I would like to record the following fact, which is hard to find on the internet: every subgroup is an equalizer, constructively. In other words, all monos in the category of groups are regular, constructively. It is interesting that this fact fails if we work in a meta-theory with “poor quotients”.

→ continue reading (9 comments)

It was time I changed the old blog style to something a bit more modern. I hope you like it.

Now I just have to figure out how to port 60 blog posts from ASCIIMathML notation to something a bit friendlier that can use MathML but does not require it. What is out there? I know about jsMath. I am open to suggestions.

→ continue reading (11 comments)

In a recent post I claimed that Python's lambda construct is broken. This attracted some angry responses by people who thought I was confused about how Python works. Luckily there were also many useful responses from which I learnt. This post is a response to comment 27, which asks me to say more about my calling certain design decisions in Python crazy.

→ continue reading (62 comments)

I quite like Python for teaching. And people praise it for the lambda construct which is a bit like $\lambda$-abstraction in functional languages. However, it is broken!

→ continue reading (57 comments)

This is a short note pointing out that the recent paper on“Mathematical undecidability and quantum randomness” by Tomasz Paterek et al. is no black magic, and that the authors are well aware of it. Unfortunately the paper appeared on Slashdot and has since generated an infinite amount of quasi-mathematical discussions.

→ continue reading (2 comments)

Today I lectured about the Hydra game by Laurence Kirby and Jeff Paris (Accessible Independence Results for Peano Arithmetic, Kirby and Paris, Bull. London Math. Soc. 1982; 14: 285-293). For the occasion I implemented the game in Java. I am publishing the code for anyone who wants to play, or use it for teaching.

→ continue reading (23 comments)

Paul Taylor has published a revised version of his `lambda`-calculus for real analysis. I recommend it to anyone who is interested in real analysis, be it a computer scientist, numerical analyst, or just a “true” analyst.

The first, second, and third time I talked to Paul I could not understand a word of what he was saying, and that's not just because he is a native speaker of English English. I only began to “get it” when he visited me in Ljubljana. So I think it's perhaps worth explaining a bit what this “`lambda`-calculus for real analysis” is about.

→ continue reading (7 comments)

The famous theorem by Cantor states that the cardinality of a powerset $P(A)$ is larger than the cardinality of $A$. There are several equivalent formulations, and the one I want to consider is

Theorem (Cantor): There is no onto map $A \to P(A)$.

In this post I would like to analyze the usual proof of Cantor's theorem and present an insightful reformulation of it which has applications outside set theory.

→ continue reading (6 comments)

Recently there has been a discussion (here, here, here, and here) on the Foundations of Mathematics mailing list about completeness of Peano arithmetic (PA) with respect to “small” sentences. Harvey Friedman made several conjectures of the following kind: “All true small sentences of PA are provable.” He proposed measures of smallness, such as counting the number of distinct variables or restricting the depth of terms. Here are some statistics concerning such statements.

→ continue reading (9 comments)

Spaces of higher-order functions are fascinating mathematical objects that we do not know enough about. What are they and what is known about them?

→ continue reading (3 comments)

Computer algebra systems (CAS), such as Mathematica, are complex systems that have been evolving for a couple of decades. They are advertised as advanced mathematical tools, and users expect them to be such. They are the next-generation calculators. But they also suffer from serious design flaws.

→ continue reading (6 comments)

So I decided to put all my research papers on the blog. → continue reading

The new address for Math and Computation blog is math.andrej.com → continue reading

I have found a good way to write math in web pages. ASCIIMathML is a piece of javascript that translates simple-minded Latex-like ASCII math to MathML, but only if the browser supports MathML. Since the input syntax is very simple, the expressions are quite readable in the raw form, as well.

For example, if I type

`forall x in RR exists y in CC. (1-x^2 )/sqrt(1+y^4)=1`

it is seen as `forall x in RR exists y in CC. (1-x^2 )/sqrt(1+y^4)=1`. If you are going to post to the blog, you may be interested in the ASCIIMathML syntax reference page.

To enable MathML on your computer, install mathplayer plugin
if you are using Internet Explorer. For Firefox and Mozilla, you have to install math fonts.

→ continue reading (2 comments)

I recently stumbled upon a blog on machine learning by a good friend of mine, John Langford. The blog has gathered together a community of people who discuss various topics (not limited strictly to machine learning). Naturally I wanted to have a blog, too.

I devote a lot of my time to thinking about the relationship between mathematics and computation. There are two sides of this, which can be expressed by a the slogan “Computable mathematics and mathematics of computation”. Computable mathematics is about how to do mathematics with computers, while mathematics of computation is about mathematics that describes properties of computation in a mathematical, abstract way.

If this is a subject that interests you, I invite you to join me.

→ continue reading (2 comments)