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 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?
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've been writing [libsodium](https://doc.libsodium.org/) bindings in Lean4 and have ended up using `native_decide` quite liberally, mostly as a convenience. Can any Lean devs provide a more thorough interrogation of this? Should I go back and try to scrub its usage out of my library? Logically it seems consistent with what I'm trying to do with Lean4's FFI (i.e. you really do need to explicitly trust the Lean kernel since I'm adding nontrivial computation using a foreign cryptography library) but I'm curious if this isn't necessary and whether Lean devs would push back on its use.
Note that the word "coordinate" used here feels a bit disingenuous to me, because that's how one might refer to the nth property defining a mathematical object or another.
For example: The third coordinate of the rational number 1/2 is a bijection.
Coordinate here actually means: third property in the definition of a rational number in Lean. Here, this property is the statement that the denominator 2 is not zero. This is not so absurd, if we define a rational number as a tuple consisting of a natural number for the numerator (property 1) and an integer for the denominator (property 2), with the added restrictions that the denominator is not the integer zero (property 3), and that the numerator and denominator are in least terms (property 4).
But the part where the proof that the denominator is nonzero can be viewed as a bijective function, is to me indeed type-theoretic weirdness. If I'm not wrong, it's just the proof viewed as a zero-argument function. (proofs for theorems that begin with e.g. forall are functions that take arguments).
It seems to me that junk theorems are fundamentally a manifestation of leaky abstractions. It happens when you can see the implementation details from inside the abstraction.
10 comments
[ 3.2 ms ] story [ 34.3 ms ] thread[1] https://www.cantorsparadise.com/what-are-junk-theorems-29868...
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...
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?
What is a coordinate in the context of a rational number? How many coordinates does it have?
For example: The third coordinate of the rational number 1/2 is a bijection.
Coordinate here actually means: third property in the definition of a rational number in Lean. Here, this property is the statement that the denominator 2 is not zero. This is not so absurd, if we define a rational number as a tuple consisting of a natural number for the numerator (property 1) and an integer for the denominator (property 2), with the added restrictions that the denominator is not the integer zero (property 3), and that the numerator and denominator are in least terms (property 4).
But the part where the proof that the denominator is nonzero can be viewed as a bijective function, is to me indeed type-theoretic weirdness. If I'm not wrong, it's just the proof viewed as a zero-argument function. (proofs for theorems that begin with e.g. forall are functions that take arguments).