7 ms·

Some Junk Theorems in Lean

91 points by saithound 10mo ago

andyjohnson0 10mo ago
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-298687b577bf https://www.cantorsparadise.com/what-are-junk-theorems-29868...
- akoboldfrying 10mo ago
  This was helpful, thanks.
  - cmrx64 10mo ago
    the last paragraphs cite why junk theorems are objectionable but then fully misinterprets it to draw the opposite conclusion. the intersection is the S-feature and problematic. 1 + 2 = 4 is a “theorem beyond T” expressed in T theory. don’t be mislead about what a junk theorem is!
    - doug-moen 10mo ago
      Yah, I read that and thought "this seems like gibberish: maybe I am reading LLM slop".
    - meroes 10mo ago
      Thank you. I was following along until that paragraph and got the opposite interpretation too.
- oersted 10mo ago
  This is very interesting. What happens if you keep pulling the thread and construct large theories on such abstraction-layer-breaking theorems? Would we arrive at interesting things like pulling the thread on sqrt(-1) for imaginary numbers? Or is it somehow “undefined behavior”, quirks of the various implementation substrates of abstract mathematics that should be (informally) ignored? My gut says the former. Are the various alternative axiomatic foundations also equivalent at this level or not? I suppose they are since they can implement/emulate each other, not sure.
- ttctciyf 10mo ago
  Maybe I'm too familiar with the set theoretic construction of the natural numbers (0 is the empty set, 1 = {0}, ..., 5 = {0,1,2,3,4}, etc.) but their example of "3 ∩ 4 = 3" or "4 intersect 3 is 3" doesn't seem weird, problematic or even useless to me, it just looks like a handy set theoretic implementation of the min() function.
  - Maxatar 10mo ago
    By itself it's not a problem, but it's certainly useless. Perhaps you can tell me what use "3 ∩ 4 = 3" has. The problem is that these properties get in the way of proving arithmetic theorems because if you are being absolutely strict, you have to distinguish things that are true of natural numbers as an algebraic structure, from things that just happen to be the case because you picked some specific representation to use for natural numbers. This introduces a lot of noise and makes formal proofs very frustrating, somewhat like when you're programming and you have to bend the type system of your compiler to accept your code even though the program is conceptually correct and you end up spending effort on type coercions, casts, "unsafe" blocks etc... mathematically this makes your proof significantly longer, more brittle, and harder to reuse because it accidentally depends on details of the chosen encoding rather than on the intrinsic properties of arithmetic.
    - ttctciyf 10mo ago
      > Perhaps you can tell me what use "3 ∩ 4 = 3" has. As I said: > a handy set theoretic implementation of the min() function. i.e. if you wanted (for whatever reason) to define min(a, b) directly and briefly in your set theoretic reconstruction of the natural numbers, you can just use intersect operator and define it as "a ∩ b". Perhaps because in terms of the interesting distinction you introduce: > you have to distinguish things that are true of natural numbers as an algebraic structure, from things that just happen to be the case because you picked some specific representation to use for natural numbers this particular operation seems to be part of the former rather than of the latter.
  - sixo 10mo ago
    It's a leaky abstraction, in software terms. Ideally, an abstraction models the semantics of the problem domain "opaquely"; ideally our natural numbers have only the properties of the natural numbers and no others. An additional property leaking through is not like handy "bonus", but a point of confusion. You can't rely on it in proofs involving natural numbers without being careful to delineate which conclusions follow from the construction vs. which are inherent.
emil-lp 10mo ago
I don't understand. What does this mean? Theorem 6. The following are equivalent: The binary expansion of 7.
- silasdavis 10mo ago
  The following are equivalent:
- bzax 10mo ago
  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.
- tux3 10mo ago
  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. S̶o̶ ̶t̶h̶e̶ ̶f̶o̶l̶l̶o̶w̶i̶n̶g̶ ̶e̶l̶e̶m̶e̶n̶t̶s̶ ̶o̶f̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶ ̶a̶r̶e̶ ̶a̶l̶l̶ ̶e̶q̶u̶i̶v̶a̶l̶e̶n̶t̶ ̶t̶o̶ ̶e̶a̶c̶h̶ ̶o̶t̶h̶e̶r̶ ̶(̶t̶h̶e̶r̶e̶ ̶i̶s̶ ̶a̶ ̶s̶i̶n̶g̶l̶e̶ ̶e̶l̶e̶m̶e̶n̶t̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶)̶
  - cmrx64 10mo ago
    the binary expansion of 7 has three elements (you will find them at indexes Fin 0, Fin 1, and Fin 2) and the proof is of their equality.
    - alimw 10mo ago
      The proof is actually of their equivalence as propositions. This is only possible because the binary digits are represented as Bools, and a Bool b can be coerced to the proposition that b = true.
- cmrx64 10mo ago
  List.TFAE is a helper definition and it’s invoked on a funny looking term when translated directly into english. I don’t know what I think, yeah it’s kinda junky but not in the way that 57 \mem 100 in a set encoding of the naturals. theorem TFAE_7_binary : List.TFAE (7).bits := by unfold Nat.bits Nat.binaryRec Nat.binaryRec; simp!
414owen 10mo ago
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...
frotaur 10mo 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?
- akoboldfrying 10mo ago
  I don't understand why they would make such footgun functions either, especially because (IIUC, and I probably don't) in a way the whole point of Lean's dependent type system is to be able to express arbitrary constraints on the inputs of these functions so that they can be total -- e.g., to be able to define a subtraction function on the nonnegative integers that takes one integer and one {integer that is less than or equal to the first integer}. And to even call this function, you (or perhaps Lean itself) would need to first prove that its second argument is less than or equal to its first.
  - Smaug123 10mo ago
    You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.) The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives! The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.
    - 10mo ago
pron 10mo ago
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).
- falcor84 10mo ago
  > 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 Note that this is actually how the basic ZF construction works, where 0 = {} and successor(n) = n ∪ {n}, so you immediately get 2 = {0, 1} and thus 1 ∈ 2 , without any need for a proof.
  - pron 10mo ago
    Except it suffices to know that some construction that supports the integer/natural axioms exists without having any specific theorems, such as 1 ∈ 2, about its specifics. In fact, in TLA+, which contains a formalised set theory, the construction is not part of the definition of the integers, and 1 ∈ 2 (or any other theorem about the construction of the integers) is not provable (of course, 1 ∉ 2 is not provable, either). The details of the construction can remain unknowable. Anyway, my point is that type theories contain at least as many junk theorems as set theories, if not more, and junk theorems are fine either way. Neither approach is more philosophically pure. Any claims to that effect are really an expression of personal aesthetic preferences.
bjt12345 10mo ago
I'm surprised to learn that lean defines the natural number 1/0 as 0.
- istjohn 10mo ago
  Doesn't this allow one to prove x=y for any x, y? x/0 = x(1/0) = x*0 = 0, so x/0 = 0 for all x. So x/0 = y/0. Multiply both sides by 0: x = y.
  - deleted 10mo ago
    [deleted]
  - deleted 10mo ago
    [deleted]
  - rnhmjoj 10mo ago
    No, because x/y is just an arbitrary operation between x and y. Here you're assuming that 1/x is the inverse of x under *, but it's not.
    - orbifold 10mo ago
      I mean in a normal math curriculum you would define only the multiplicative inverse and then there is a separate way to define fraction, if you start out with certain rings. It is kind of surprising to me that they did a lazy definition of division.
  - Smaug123 10mo ago
    What theorem did you use that allowed you to multiply both sides by $0$? (That theorem had conditions on it which you didn't satisfy.)
- zodiac 10mo ago
  Here’s a good document defending the merits of this design. https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
proof_by_vibes 10mo ago
I've been writing [libsodium](https://doc.libsodium.org/ 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.
teiferer 10mo ago
> Theorem 1. The third coordinate of the rational number 1/2 is a bijection. What is a coordinate in the context of a rational number? How many coordinates does it have?
jhanschoo 10mo ago
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).
- dernett 10mo ago
  Lean defines a != b as a = b => False, so it seems that we have a function from proofs of a = b to proofs of False. I guess this being bijective means that there are no proofs of a = b, since there are no proofs of False, which is an equivalent way of looking at a != b.
fsmv 10mo ago
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.

91 points by saithound 10mo ago

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-298687b577bf https://www.cantorsparadise.com/what-are-junk-theorems-29868...

akoboldfrying 10mo ago
This was helpful, thanks.
- cmrx64 10mo ago
  the last paragraphs cite why junk theorems are objectionable but then fully misinterprets it to draw the opposite conclusion. the intersection is the S-feature and problematic. 1 + 2 = 4 is a “theorem beyond T” expressed in T theory. don’t be mislead about what a junk theorem is!
  - doug-moen 10mo ago
    Yah, I read that and thought "this seems like gibberish: maybe I am reading LLM slop".
  - meroes 10mo ago
    Thank you. I was following along until that paragraph and got the opposite interpretation too.
oersted 10mo ago
This is very interesting. What happens if you keep pulling the thread and construct large theories on such abstraction-layer-breaking theorems? Would we arrive at interesting things like pulling the thread on sqrt(-1) for imaginary numbers? Or is it somehow “undefined behavior”, quirks of the various implementation substrates of abstract mathematics that should be (informally) ignored? My gut says the former. Are the various alternative axiomatic foundations also equivalent at this level or not? I suppose they are since they can implement/emulate each other, not sure.
ttctciyf 10mo ago
Maybe I'm too familiar with the set theoretic construction of the natural numbers (0 is the empty set, 1 = {0}, ..., 5 = {0,1,2,3,4}, etc.) but their example of "3 ∩ 4 = 3" or "4 intersect 3 is 3" doesn't seem weird, problematic or even useless to me, it just looks like a handy set theoretic implementation of the min() function.
- Maxatar 10mo ago
  By itself it's not a problem, but it's certainly useless. Perhaps you can tell me what use "3 ∩ 4 = 3" has. The problem is that these properties get in the way of proving arithmetic theorems because if you are being absolutely strict, you have to distinguish things that are true of natural numbers as an algebraic structure, from things that just happen to be the case because you picked some specific representation to use for natural numbers. This introduces a lot of noise and makes formal proofs very frustrating, somewhat like when you're programming and you have to bend the type system of your compiler to accept your code even though the program is conceptually correct and you end up spending effort on type coercions, casts, "unsafe" blocks etc... mathematically this makes your proof significantly longer, more brittle, and harder to reuse because it accidentally depends on details of the chosen encoding rather than on the intrinsic properties of arithmetic.
  - ttctciyf 10mo ago
    > Perhaps you can tell me what use "3 ∩ 4 = 3" has. As I said: > a handy set theoretic implementation of the min() function. i.e. if you wanted (for whatever reason) to define min(a, b) directly and briefly in your set theoretic reconstruction of the natural numbers, you can just use intersect operator and define it as "a ∩ b". Perhaps because in terms of the interesting distinction you introduce: > you have to distinguish things that are true of natural numbers as an algebraic structure, from things that just happen to be the case because you picked some specific representation to use for natural numbers this particular operation seems to be part of the former rather than of the latter.
- sixo 10mo ago
  It's a leaky abstraction, in software terms. Ideally, an abstraction models the semantics of the problem domain "opaquely"; ideally our natural numbers have only the properties of the natural numbers and no others. An additional property leaking through is not like handy "bonus", but a point of confusion. You can't rely on it in proofs involving natural numbers without being careful to delineate which conclusions follow from the construction vs. which are inherent.

emil-lp 10mo ago

I don't understand. What does this mean? Theorem 6. The following are equivalent: The binary expansion of 7.

silasdavis 10mo ago
The following are equivalent:
bzax 10mo ago
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.
tux3 10mo ago
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. S̶o̶ ̶t̶h̶e̶ ̶f̶o̶l̶l̶o̶w̶i̶n̶g̶ ̶e̶l̶e̶m̶e̶n̶t̶s̶ ̶o̶f̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶ ̶a̶r̶e̶ ̶a̶l̶l̶ ̶e̶q̶u̶i̶v̶a̶l̶e̶n̶t̶ ̶t̶o̶ ̶e̶a̶c̶h̶ ̶o̶t̶h̶e̶r̶ ̶(̶t̶h̶e̶r̶e̶ ̶i̶s̶ ̶a̶ ̶s̶i̶n̶g̶l̶e̶ ̶e̶l̶e̶m̶e̶n̶t̶ ̶i̶n̶ ̶t̶h̶e̶ ̶l̶i̶s̶t̶)̶
- cmrx64 10mo ago
  the binary expansion of 7 has three elements (you will find them at indexes Fin 0, Fin 1, and Fin 2) and the proof is of their equality.
  - alimw 10mo ago
    The proof is actually of their equivalence as propositions. This is only possible because the binary digits are represented as Bools, and a Bool b can be coerced to the proposition that b = true.
cmrx64 10mo ago
List.TFAE is a helper definition and it’s invoked on a funny looking term when translated directly into english. I don’t know what I think, yeah it’s kinda junky but not in the way that 57 \mem 100 in a set encoding of the naturals. theorem TFAE_7_binary : List.TFAE (7).bits := by unfold Nat.bits Nat.binaryRec Nat.binaryRec; simp!

414owen 10mo ago

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...

frotaur 10mo 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?

akoboldfrying 10mo ago
I don't understand why they would make such footgun functions either, especially because (IIUC, and I probably don't) in a way the whole point of Lean's dependent type system is to be able to express arbitrary constraints on the inputs of these functions so that they can be total -- e.g., to be able to define a subtraction function on the nonnegative integers that takes one integer and one {integer that is less than or equal to the first integer}. And to even call this function, you (or perhaps Lean itself) would need to first prove that its second argument is less than or equal to its first.
- Smaug123 10mo ago
  You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.) The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives! The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.
  - 10mo ago

pron 10mo ago

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).

falcor84 10mo ago
> 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 Note that this is actually how the basic ZF construction works, where 0 = {} and successor(n) = n ∪ {n}, so you immediately get 2 = {0, 1} and thus 1 ∈ 2 , without any need for a proof.
- pron 10mo ago
  Except it suffices to know that some construction that supports the integer/natural axioms exists without having any specific theorems, such as 1 ∈ 2, about its specifics. In fact, in TLA+, which contains a formalised set theory, the construction is not part of the definition of the integers, and 1 ∈ 2 (or any other theorem about the construction of the integers) is not provable (of course, 1 ∉ 2 is not provable, either). The details of the construction can remain unknowable. Anyway, my point is that type theories contain at least as many junk theorems as set theories, if not more, and junk theorems are fine either way. Neither approach is more philosophically pure. Any claims to that effect are really an expression of personal aesthetic preferences.

bjt12345 10mo ago

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

istjohn 10mo ago
Doesn't this allow one to prove x=y for any x, y? x/0 = x(1/0) = x*0 = 0, so x/0 = 0 for all x. So x/0 = y/0. Multiply both sides by 0: x = y.
- deleted 10mo ago
  [deleted]
- deleted 10mo ago
  [deleted]
- rnhmjoj 10mo ago
  No, because x/y is just an arbitrary operation between x and y. Here you're assuming that 1/x is the inverse of x under *, but it's not.
  - orbifold 10mo ago
    I mean in a normal math curriculum you would define only the multiplicative inverse and then there is a separate way to define fraction, if you start out with certain rings. It is kind of surprising to me that they did a lazy definition of division.
- Smaug123 10mo ago
  What theorem did you use that allowed you to multiply both sides by $0$? (That theorem had conditions on it which you didn't satisfy.)
zodiac 10mo ago
Here’s a good document defending the merits of this design. https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer...

proof_by_vibes 10mo ago

I've been writing [libsodium](https://doc.libsodium.org/ 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.

teiferer 10mo ago

> Theorem 1. The third coordinate of the rational number 1/2 is a bijection. What is a coordinate in the context of a rational number? How many coordinates does it have?

jhanschoo 10mo ago

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).

dernett 10mo ago
Lean defines a != b as a = b => False, so it seems that we have a function from proofs of a = b to proofs of False. I guess this being bijective means that there are no proofs of a = b, since there are no proofs of False, which is an equivalent way of looking at a != b.

fsmv 10mo ago

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.