Some Junk Theorems in Lean
github.com28 points by saithound 4 days ago
28 points by saithound 4 days ago
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...
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 understand. What does this mean?
Theorem 6. The following are equivalent: The binary expansion of 7.This is a junk theorem, it's trying to prove something that will sound strange or meaningless but is technically allowed by the details of the foundations.
Here it's building a list with one element and saying all elements of this list are equivalent. So the following elements of the list are all equivalent to each other (there is a single element in the list)
It doesn't mean anything. The point is that the language of lean, and its proof derivation system, are able to express (and prove) statements that do not correspond to any meaningful mathematics.