## Hey! I heard that Lean thinks 1/0 = 0. Is that true?

Yes. So do Coq and Agda and many other theorem provers.

## Doesn’t that lead to contradictions?

No. It just means that Lean’s `/`

symbol doesn’t mean mathematical division. Let denote the real numbers. Let’s define a function by if and . Does *making that definition* give us a contradiction in mathematics? No, of course not! It’s just a definition. Lean uses the symbol `/`

to mean . As does Coq, Agda etc. Lean calls it `real.div`

by the way, not .

## But doesn’t that lead to confusion?

It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians **don’t divide by 0** and hence in practice they never notice the difference between `real.div`

and mathematical division (for which `1/0`

is undefined). Indeed, if a mathematician is asking what Lean thinks `1/0`

is, one might ask the mathematician *why they are even asking,* because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work. In fact knowing `real.div`

is the same as knowing mathematical division; any theorem about one translates into a theorem about the other, so having `real.div`

is equivalent to having mathematical division.

## This convention is stupid though!

It gets worse. There’s a subtraction `nat.sub`

defined on the natural numbers , with notation `x - y`

, and it eats two natural numbers and spits out another natural number. If `x`

and `y`

are terms of type `ℕ`

and `x < y`

, then `x - y`

will be 0. There’s a function called `real.sqrt`

which takes as input a real number, and outputs a real number. If you give it , it outputs . I don’t know what happens if you give it the input , beyond the fact that it is guaranteed to output a real number. Maybe it’s 0. Maybe it’s 1. Maybe it’s 37. I don’t care. I am a mathematician, and if I want to take the square root of a negative real number, I won’t use `real.sqrt`

because I don’t want an answer in the reals, and the type of `real.sqrt`

is `ℝ → ℝ`

.

## Why can’t you just do it the sensible way like mathematicians do?

Great question! I tried this in 2017! Turns out it’s *really inconvenient in a theorem prover!*

Here’s how I learnt Lean. I came at it as a “normal mathematician”, who was thinking about integrating Lean into their undergraduate introduction to proof course. I had no prior experience with theorem provers, and no formal background in programming. As a feasibility study, I tried to use Lean to do all the problem sheets which I was planning on giving the undergraduates. This was back in 2017 when Lean’s maths library was much smaller, and `real.sqrt`

did not yet exist. However the basic theory of sups and infs had been formalised, so I defined `real.sqrt x`

, for `x`

non-negative, to be , and proved the basic theorems that one would want in an interface for a square root function, such as and and and so on (here are non-negative reals, the only reals which my function would accept).

I then set out to prove , a question on a problem sheet from my course. The students are told not to use a calculator, and asked to find a proof which only uses algebraic manipulations, i.e. the interface for `real.sqrt`

. Of course, the way I had set things up, **every time** I used the symbol I had to supply a proof that what I was taking the square root of was non-negative. Every time the symbol occurred in my proof. Even if I had proved `2 > 0`

on the previous line, I had to prove it again on this line, because this line also had a in. Of course the proof is just `by norm_num`

, but that was 10 characters which I soon got sick of typing.

I then moaned about this on the Lean chat, was mocked for my silly mathematician conventions, and shown the idiomatic Lean way to do it. The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the **theorems** where one puts the non-negativity hypotheses. For example, the statement of the theorem that has the hypotheses that . Note that it does *not* also have the hypothesis that , as one can deduce this within the proof and not bother the user with it. This is in contrast to the mathematicians’ approach, where the proof that would also need to be supplied because it is in some sense part of the notation.

## So you’re saying this crazy way is actually *better*?

No, not really. I’m saying that it is (a) *mathematically equivalent* to what we mathematicians currently do and (b) simply *more convenient* when formalising mathematics in dependent type theory.

What actually is a field anyway? For a mathematician, a field is a set equipped with where the inversion function is only defined for non-zero . The non-zero elements of a field form a group, so we have axioms such as for (and this doesn’t even make sense for ). Let’s say we encountered an alien species, who had also discovered fields, but their set-up involved a function instead of our . Their was defined, using our notation, by for , and . Their axioms are of course just the same as ours, for example they have for . They have an extra axiom , but this is no big deal. It’s swings and roundabouts — they define and their theorem doesn’t require , whereas ours does. They are simply using slightly different notation to express the same idea. Their is discontinuous. Ours is not defined everywhere. But there is a *canonical isomorphism of categories* between our category of fields and theirs. There is *no difference mathematically* between the two set-ups.

Lean uses the alien species convention. The aliens’ is Lean’s `field.inv`

, and Lean’s `field.div x y`

is defined to be `field.mul (x, field.inv y)`

.

## OK so I can see that it can be made to work. Why do I still feel a bit uncomfortable about all this?

It’s probably for the following reason. You are imagining that a computer proof checker will be checking your work, and in particular checking to see if you ever divided by zero, and if you did then you expect it to throw an error saying that your proof is invalid. What you need to internalise is that Lean is just using that function above, defined by for and . In particular you cannot prove false things by applying to an input of the form , because the way to get a contradiction by dividing by zero and then continuing will involve invoking theorems which are true for mathematical division but which are not true for . For example perhaps a mathematician would say is true for all , with the implicit assumption that and that this can be inferred from the notation. Lean’s theorem that `real.div a a = 1`

is only proved under the assumption that , so the theorem cannot be invoked if . In other words, the problem simply shows up at a different point in the argument. Lean won’t accept your proof of which sneakily divides by 0 on line 8, but the failure will occur at a different point in the argument. The failure *will still however be the assertion that you have a denominator which you have not proved is nonzero.* It will simply not occur at the point when you do the division, it will occur at the point where you invoke the theorem which is not true for `real.div`

.

Thanks to Jim Propp and Alex Kontorovich for bringing this up on Twitter. I hope that this clarifies things.

I don’t think Agda adopts this convention!

LikeLiked by 1 person

I like this post but disagree with the conclusion. IMHO, “1 / 0 = 0” is actually the least harmful of such statements. “0 – 1 = 0” and “1 / 2 = 0” are much worse, for two reasons:

* When read literally, these are simply false (mathematically). Of course, Lean wants us to use e.g. “(0 : ℤ) – (1 : ℤ)” instead, but if “0 – 1” does not mean the same thing, that increases the chance that some formalized definition or theorem does not say what it is intended to say.

* It makes subtraction of natural numbers incompatible with subtraction of integers. Mathematically, when introducing the integers, we _extend_ the definition of subtraction to ℤ. But Lean’s “-” on integers does not extend “-” on natural numbers on its entire domain.

I think it’s possible to do better. If the “correct” mathematical definitions are inconvenient to work with, changing the definitions is one answer, another answer would be that it’s the proof assistant’s job to make it more convenient. In particular if, as you say, most of the required proofs are trivial.

As I understand, in Lean there are two different reasons for the inconvenience:

* Working with subtypes is inconvenient in general. (With subtypes, we can write the “correct” definitions as e.g.:)

def nat_leq (n : ℕ) := {m : ℕ // m ≤ n}

def sub’ (n : ℕ) (m : nat_leq n) := n – subtype.val m

* The clutter caused by trivial proofs.

A proof assistant I’m working on (https://sreichelt.github.io/slate) aims to solve both issues. E.g. here are the definitions of subtraction and division of natural numbers:

* https://slate-prover.herokuapp.com/libraries/hlm/Essentials/Numbers/Natural/difference

* https://slate-prover.herokuapp.com/libraries/hlm/Essentials/Numbers/Natural/quotient

Using these definitions does require “inline” proofs, but only if the constraints are not trivially satisfied in the current context. (This is work in progress, though.)

LikeLike

I think that maybe custom notation would be a good answer. Some kind of weird thing which looks a bit like subtraction/division but isn’t. But the CS people got there first.

LikeLike

I agree. Apparently, there is actually an established symbol for truncated subtraction: https://en.wikipedia.org/wiki/Monus

Having this symbol all over the source code would be really strange, though. My guess is that the next thing people would want is a notation “-” that works as expected but doesn’t cast to integer unless necessary.

LikeLike

Your proof assistant looks superb! I started to lose faith in Lean… 😉

LikeLike

This now touches upon a different question. Out of all the provers — which one should mathematicians be putting their time into? Of course this is assuming that they should be putting their time into any of them! For the last 30 years this has not been happening to any great extent.

I am generally pushing the idea that mathematicians should engage with theorem provers, but of course I have also decided to push Lean, and this is because I personally think that it’s the one which can currently best handle the areas I’m interested in; it’s the one for which the design decisions seem to be closest to the principles I work with as an arithmetic geometer (and in particular my strong rejection of constructivism). However I am not blind enough to think that Lean is the one chosen prover and that no other prover before or since will be able to compete. One of the reasons I think that it is so fundamentally important to get an undergraduate maths degree program and more into Lean is that doing this will show us what works well in dependent type theory, and what works badly. When it comes to things like C^infty manifolds, or gluing sheaves on topological spaces, or defining group cohomology/de Rham cohomology/singular cohomology, I think that this is a very poorly understood question. Sebastian I would absolutely encourage you to work on “yet another prover” because new provers can be made building on what we have learnt from experiments with older ones.

LikeLike

FWIW, truncating subtraction is the mathematically correct definition of subtraction on the natural numbers, since that is the definition which is adjoint to addition (in the posetal category where objects are natural numbers and the homs are given by the ordering on natural numbers). You get the integers (and the primary school notion of subtraction) when you hit this category of natural numbers with the Grothendieck group construction.

My own experience with mechanised proof is that it really rewards using a “mathematically mature” approach even when formalizing basic concepts, because that’s the approach which makes latent algebraic structure explicit and visible to the proof assistant, and hence available to use for the purposes of automation.

Like Martin says, you should be wary when you find yourself making choices to please the machine rather than the mathematician. The compromise I am content with is to listen to the machine when it asks me to do math better, but to be resistant when it asks me to make unmotivated choices.

LikeLike

Also, this is an example where you make a definition for technological reasons to adapt to computer programs rather than for conceptual mathematical reasons. You said “that was 10 characters which I soon got sick of typing.”. But then you had to write many more than 10 characters in the above post to explain this mathematically strange convention. Moreover, if you are using this to teach undergrads, as you are, you will have to explain why “1/0” doesn’t make sense mathematically, and why you define it to be “0” anyway “for convenience”. Also this bad use of conventions gives a bad name to the software systems for theorem proving, when in reality, as you explained, it is the people using them that adopt such strange conventions. If we don’t adopt such a convention in real mathematics, why would we do it when formalizing it? The formalization of mathematics should be as close as possible to the way we think about it, not a new way of doing it better adapted to currently available support. If you want to save 10 characters, *the computer* should offer better support.

LikeLike

We could set it up the mathematical way, and have 1/0 literally not make sense. Your comments are very interesting Martin — it had not really occurred to me that there was any reason to do this

LikeLike

> But there is a canonical isomorphism of categories between our category of fields and theirs. There is no difference mathematically between the two set-ups.

so basically you are treating these categories as equal? 🙂 There’s a certain Japanese mathematician you should talk to …

LikeLike

Pingback: Small observations on fields in Lean – theHigherGeometer

I chose my words carefully: I was initially going to write “equivalence of categories” but then I realised that in this case it was actually much stronger.

LikeLiked by 1 person