3 ms·
I don't understand. What does this mean? Theorem 6. The following are equivalent: The binary expansion of 7.
by 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 agoThe following are equivalent:
- bzax 10mo agoIt 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 agoThis 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 agothe 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 agoThe 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 agoList.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!
- homeless_engi 10mo agoAs I think another commenter hinted, the binary expansion of 7 is 111. And indeed, 1 = 1 = 1
- SkiFire13 10mo agoIt's more like "the bits of 7 are all equivalent", which is kinda obvious when you notice that they are `111`