Some Junk Theorems in Lean

I don't know much about Lean, but I attended an introductory talk at some point and I was particularly bothered by these partial function definitions. The example was sqrt, which would give 0 on the negatives.

Now, of course, if you're careful with the definitions you use, there is no problem. But in the (increasingly relevant) context of automatic theorem proving with LLMs, this seems to defeat the 'groundtruthness' of Lean!

How do you make sure that the LLM doesn't reward hack a proof using these workarounds?

TIL that "junk theorems" are a thing in mathematics. Not being a mathematician myself, I found this [1] article a useful primer.

[1] https://www.cantorsparadise.com/what-are-junk-theorems-29868...

I'm surprised to learn that lean defines the natural number 1/0 as 0.

Wow, okay. I would imagine this makes mathematicians quite angry? I guess you're responsible for all the operations you use in your proof being well-behaved.

It sounds like subtraction over Nats needs to be split into `sub?`, and `sub!`, the former returning an option, and the latter crashing, on underflow, as is the Lean convention?

To use the default `sub`, you should need to provide a witness that the minuend is >= the subtrahend...

The version with silent underflow is still useful, it should just be called `saturatingSub`, or something, so that mathematicians using it know what they're getting themselves into...

I don't think anyone minds this. The purpose of a formal foundation is to prove useful theorems. Junk theorems are just a side effect. But I'm always tickled by logicians who think type theories are philosophically superior to set theories because in some of the latter you might be able to prove something like 1 ∈ 2, whereas type theories, even without their own junk theorems, have a pragmatic difficulty with division (hence they tend to define 1/0 = 0). Junk theorems just come with the territory, and foundations need to be considered based on their utility, not philosophical purity, which is never achieved anyway (at least not without a cost to utility).

I don't understand. What does this mean?

    Theorem 6. The following are equivalent: The binary expansion of 7.