Formalising Mathematics: An Introduction

After working with Lean for a while, I've started to appreciate that there is a wider range of what it means to be constructive -- being "fully constructive" seems to me to be like fanatical efforts to make everything X, for example "everything is a function" or "everything is an object" and so on.

In the Lean approach, anything not marked `noncomputable` in the Type universe and above needs to be constructible, in the sense that there is a program that can compute such an object using a functional programming language (where the function is guaranteed to terminate), but proofs don't need to be constructible in the same way. Proofs are still functions, but they're free to use things like the axiom of choice in the course of a proof. The way things are set up, even if you use non-computable things while making your inferences, this "forbidden" data will not leak out.

It seems eminently reasonable to me that you can argue a program computes the correct thing because it doesn't compute the wrong thing, and unless you're specifically studying different toposes/logics, I'm not sure what constructive logic would really give you (and it's not like mathematicians slavishly keep track of where they used the axiom of choice or its consequence the LEM).

How this all looks in Lean practice is that it's stronger to give a definition and prove it satisfies a property than to prove a "there exists" statement. mathlib authors tend to go for the first, unless the result is inherently noncomputable. There's also a facility for lifting propositions up to boolean values, which more or less amounts to giving a constructive proof -- this is used pervasively, for example with finite sets, which are constructive in the sense that if you have one there's an actual finite list backing it.

I guess in short: it's a useful middle ground being able to prove something exists without having to construct it, but if you want to "have" the thing that purportedly exists you need to construct it.

It's mathematics where certain kinds of proof by contradiction are not allowed -- if you want to prove that something exists because you want to use it, then you have to make it, you can't just say "let's assume it didn't exist and go on from there to deduce that 0 = 1 which is definitely wrong, so our assumption is wrong, so it exists, so let's use it".

Here is the reason why it's obvious for mathematicians. If you're trying to prove a theorem (e.g. the theorem that class numbers of imaginary quadratic fields tend to infinity), and then someone comes up with a proof which assumes that a certain generalisation of the Riemann hypothesis is true, and then someone else comes up with a proof which assumes that the exact same generalisation is false, then we mathematicians say "great, the theorem is now proved". This actually happened.

However if your boss asks you to write some code which does a calculation, and the next day you show up in their office with two USB sticks and say "this code is guaranteed to produce the correct answer if the Riemann hypothesis is true, and this other code is guaranteed to produce the correct answer if the Riemann hypothesis is false" then you are going to lose your job, because all you did was prove that the code exists, which is less helpful than it could be.

For me one of the biggest problems with the area of formalisation of mathematics is that for decades it has been dominated by computer scientists, whose view of what is important and beautiful in mathematics does not really coincide with that of the working mathematician. This is what I am fighting to change.

> This actually happened

Oh wow! Was it an interesting theorem that got proved this way? Did it get proved in another, less controversial manner as well? Could you provide a pointer to it?

There does not seem to be any reason for mathematicians to be turned about by these engines using constructive mathematics. One can use excluded middle as an axiom and do all the classical mathematics one likes. What becomes much easier if the engine is constructive is telling which theorems depend on excluded middle and which do not.

I absolutely love everything about this. Specially how it can provide access to knowledge to people all around the world.

I'm currently thinking about getting a degree in Maths, and I find extremely appealing the notion of having a repo of knowledge from where to gather theorems, specially useful for newer developed areas.