You're referring to this reddit post.

    #eval (1/0 : Nat) -- 0
    #eval (1/0 : Int) -- 0

It's one of the best places! You know how in programming, your code looks like this?

    func my_function(inputs) -> output  { do something }

    theorem my_theorem(assumptions) -> conclusion { prove something }

So as long as your assumptions and conclusion don't involve any division by zero, it doesn't matter what goes on inside the proof.

Regarding division by zero, you sort of have three options:

* Output an error / checked null when there's division by zero.

* Require a proof that the denominator is nonzero before you're even allowed to use division.

* Allow division by zero, making it return some nonsense. Then, add an assumption that the denominator is nonzero to all your theorems about division.

The first two options (especially the second one) make the definition of functions that involve division horrifically messy. (Idk, it might be easier if Lean had exceptions, but that also sounds messy.) I think that's why Lean goes with the third option.

https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

Trying to solve the problem with e.g. dependent typechecking quickly gets complicated (both implementation and theory). And adding a concept such as infinity may complicate proofs which now need to deal with infinity being a "number" but which behaves differently from other numbers.

Thankfully mathematics has the nice property that you can define concepts any way you want so long as they're self-consistent and match one's expectations. So rather than treating division by zero as an exceptional case -- either by disallowing it in the typesystem, "raising an error", or by introducing a "special" value -- some (most?) verification languages simply define division by zero to have a numeric value, and make it known that this is the case. Users know that they must then write expressions to be explicit about division by zero if they care about that case. (This turns out to be not much different than having to write expressions to satisfy a dependent type system.)

More generally, in normal math, every theorem that involves division by some value Y which could be zero must have as hypothesis that Y is not equal to zero. All these theorems still work in systems like Lean where division by zero is defined to be zero, so nothing is lost.

You could write all your formulas in the Maybe / Option monad (which I guess is the same as 'introducing a "special" value') but that sounds painful...

There are good reasons for the convention of assigning nonsense values to computations that are formally invalid. The convention is so important that it is introduced in the Natural Number Game, where the remarks include a brief discussion of why the predecessor of 0 is defined to be 37.

I don't think there's any particular reason why you'd assign 0 as the nonsense value?

There are practical reasons why we leave division by 0 undefined in "normal" arithmetic but we could, just as easily, operate in a world where 1/0 is defined. In some contexts, 1/0 = 0 is a totally sensible convention! In others, we can define it to be ∞ or, hell, something else entirely.

This approach of teaching math as a bunch of universal facts that are either true or false is actively harmful—but super convenient for top-down education and assessment!—because it teaches people the wrong way to think about math or even about conceptual models in general.

Except that for all other numbers we have 1/x * x = 1, while 0*0 = 0. Defining division by zero this way breaks existing rules.

Calling the color of the sky blue is just a matter of convention as well, but if one random teacher starts calling it green, she’s doing a terrible disservice to her students. It doesn’t matter that there exists some languages without a difference between blue and green.

    ceil(0.000001) = 1
    ceil(0) =... 0? Wtf?

Right — because it’s impossible to have an inverse of zero multiplication.

Eg, 0 = 0 + 0 -> 1 = 1 + 1 -> 0 = 1 if you have a multiplicative inverse to 0, and hence you have collapsed your entire system to a single value.

These are students we’re still teaching that basic algebraic structure to — that it’s not possible to have a multiplicative inverse to zero.

Calling that a “convention” is wrong.

If you know more than others, that's great, but in that case the thing to do is to share some of what you know, so others can learn. If you don't want to do that, that's fine, but in that case please don't post. Putdowns and swipes only degrade the discussion.

https://hn.algolia.com/?dateRange=all&page=0&prefix=true&sor...

I thought the worst part is that in context of "normal" mathematics taught in schools one is obviously wrong, and also unable to do research and admit own mistakes, and that one is actually teaching children.

> This approach of teaching math as a bunch of universal facts that are either true or false is actively harmful

Kids are taught not philosophy or logic but certain mathematical paradigm (that you call "normal") in which division by zero is an error. If you have a formula you decompose it to smaller formulas, if in a smaller formula you have a division by zero you simplify it to zero then you screwed up the entire thing. There's no true or false value for 1/0, the right move is not to play and not solve any equation in which division by zero appears.

Actually, let me rephrase. It's a bad situation all-round. I assume you didn't tell your friend's kid to go in and argue with her teacher. (If you did, then you are a prick. Otherwise, I rescind the above.) At that age, kids want to tell people when they learn fun or exciting things (well, that's not really restricted to that age), but they don't always think through the effects of saying them. Now, I definitely do know a number of elementary teachers who aren't great at math, but even if the teacher is good at math, imagine their perspective. Off the top of my head, I can only think of a small number of options: 1. agree, move on, and have a bunch of kids who are either confused or are going around telling everyone they know "1 + 1 = 10" without understanding why; 2. scrap whatever lesson they were supposed to do and go into a long, unplanned explanation of how different number bases work and interact with place value; 3. tell the girl she's wrong. Quite frankly, none of these are good options.

I can't really fault you for teaching her fun math, but for an elementary teacher that's a really rough spot to be put in.

And yes, letting everyone be argumentative all the time is how classroom management goes out the window.

it's people like you that are pricks for thinking that anyone with extra learning are punishing everyone else in class. it's never a problem for keeping students ready to advance faster than the rest of class keeping them all held back at the slower pace.

you're also a prick for assuming the way the conversation came about. you're a prick for not thinking that the conversation was about how math can be fun where things that are simple and considered basic can be different and more advanced where 1+1=2 can also be 1+1=10. but now, you just go off and assume i'm a dick saying 1+1=2 is wrong and the correct answer is 1+1=10 or whatever nonsense led you to thinking i'm a prick.

I never said this and do not think this.

I was attempting to provide more nuance to the situation and evidently failed.

how about teachers should be much less aggrieved that an elementary student is probably smarter than they are. when a student shows initiative to learn something on their own, rather than being an ignorant person and send the kid to the principal's office because they think the kid made a bomb or is learning maths at a pace faster than the hayseed teacher is.

see, that whole paragraph has a point that would probably be made much more acceptable if I didn't phrase it in an insulting manner