Some Junk Theorems in Lean
Key topics
Diving into the fascinating world of "junk theorems" in mathematics, a recent GitHub repository sparked a lively discussion about the implications of Lean, a proof assistant, generating seemingly nonsensical mathematical statements. Commenters were initially confused by the examples provided, with some misinterpreting the author's conclusion, but ultimately, the thread clarified the concept: Lean's language can express and prove statements that don't correspond to meaningful mathematics. As some commenters wondered what would happen if they "kept pulling the thread" and constructed large theories on such abstraction-layer-breaking theorems, others shared their own experiences with set-theoretic constructions, highlighting the complexities and nuances of mathematical foundations.
Snapshot generated from the HN discussion
Discussion Activity
Very active discussionFirst comment
4d
Peak period
52
96-108h
Avg / period
12.2
Based on 61 loaded comments
Key moments
- 01Story posted
Dec 23, 2025 at 6:53 AM EST
10 days ago
Step 01 - 02First comment
Dec 27, 2025 at 6:45 AM EST
4d after posting
Step 02 - 03Peak activity
52 comments in 96-108h
Hottest window of the conversation
Step 03 - 04Latest activity
Dec 29, 2025 at 2:03 AM EST
4d ago
Step 04
Generating AI Summary...
Analyzing up to 500 comments to identify key contributors and discussion patterns
Want the full context?
Jump to the original sources
Read the primary article or dive into the live Hacker News thread when you're ready.
[1] https://www.cantorsparadise.com/what-are-junk-theorems-29868...
don’t be mislead about what a junk theorem is!
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.
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".
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)
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?
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.
> If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove
This is the part I'm struggling with. How would you actually know/realise that you were doing this? It seems like "the mathlib way" you describe is choosing to rely on programmer discipline for something that could be enforced automatically.
My fear is that relying on the junk values of functions (values where their "proper" partial counterparts are not defined) is somehow unsound (could lead to proving something untrue). But perhaps my intuition is off here? If so, I think the specific junk values chosen must not matter at all -- e.g., having sqrt return 42 for negative x values should work just as well, am I right?
But you're exactly right. There's nothing linking theorem prover definitions to pen and paper definitions in any formal system.
- Fewer side conditions: Setting a / 0 = 0 means that the law a * /a = 0 holds even for a = 0, and so you don't need to prove a != 0. This is super nice when the denominator is horrible. I heard once that if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions (though I didn't track down this paper to find out for sure).
- Some of the wacky junk arithmetic values, especially as it relates to extended reals, do show up in measure theory. Point being: "junk arithmetic" is a different mathematical theory than normal math, but it's no less legitimate, and is closely related.
- Definition with Hilbert's epsilon operator. If I want to define a function that takes eg. a measurable set S as an argument, I could do the dependent types way
def MyDef (S) (H : measurable S) := /-- real definition -/
but then I need to write all of my theorems in terms of (MyDef S H) and this can cause annoying unification problems (moreso in Rocq than in Lean, assuming H is a Prop). Alternatively, I could use junk math
def MyDef' (S) := if (choose (H : measurable S)) then /-- real definition -/ else /-- junk -/
I can prove (MyDef' S = MyDef S H) when I have access to (H : measurable S). And the property H here can be be really complex, convergence properties, existence properties, etc. It's nice to truck them around everywhere.
Wouldn’t this still cause problems if the lim sup is ∞ and the lim inf is -∞?
I found the last section especially helpful.
This is horrible for a language whose whole purpose I thought was that to be foolproof and that if it compiles its true. Having very subtly different definitions of common operations is such a footgun.
Of course, I understand that this doesn’t bother mathematicians because they are used to not having any guardrails anyways. Just like C programmers have the attitude that if you fall on such a trap that you deserve it and you are not a “real programmer”. But Lean is supposed to be the other extreme isn’t it? Take nothing for granted and verify it from the ground up.
I suppose I am falling for that “Twitter confusion” the post is referring to. I never had any issues with this when actually using Lean. I just don’t like the burden of having to be paranoid about this, I thought Lean had my back and I could use it fairly mechanically by transforming abstract structures without thinking about the underlying semantics too much.
In other words, you can use all these junk theorems to build strange results on the side, but you can never build something that disagrees with normal math or that contradicts itself. There is no footgun, because the weird results you obtain are just notation. They look weird to a human, but they don't allow you to actually break any rules or to prove 1=0.
More importantly, the other way around, it seems too easy to copy a proposition from paper onto Lean and falsely prove it without realising they don't express the same thing. A human probably wouldn't but there's increased usage of AI and other automatic methods with Lean.
I do understand I'm being purist and that it doesn't matter that much in practice. I've used Lean seriously for a while and I've never encountered any of this.
TL;DR: It's actually harmless (and often convenient) to "inflate" the domains of partial functions to make them total (by making them return arbitrary junk values where the original function is undefined), provided that every theorem you want to apply still comes with the original, full restrictions.
Kevin's example is good. My stupider example would be: We can define a set that contains the integers ..., -2, -1, 0, 1, 2, ..., plus the extra element "banana". If we define the result of any addition, subtraction or multiplication involving a banana to be 42, and to have their usual results otherwise, then, provided that we add the condition "None of the variables involved is banana" to the theorem "x+y = y+x", and to every other theorem about arithmetic, anything that we can prove about arithmetic on elements of this set is also true of arithmetic on integers.
(discussion: https://news.ycombinator.com/item?id=17736046)
This is usually done by PL's that want to avoid crashes at all costs, but "turning crashes into subtle logic errors" seems like a really bad idea.
"As a programmer, I don’t like it."
"As mentioned before, this is not a post about what’s practically a good idea. All I’m arguing is that mathematically, we can extend division in this way without leading to a contradiction. Programming languages are different from mathematical formalisms, and should be different. I prefer that 1/0 is an error, because I’m not using my program to prove theories."
Please do yourself a favor and actually read it.
Besides, 0 as a sentinental value on disk or on the wire is fine, but once you have values in a programming language, use option types. This is not 1980s anymore, you don't need to use 0 or -1 or 0xffff to express something special which sooner or later just falls on your feet.
Ah, that's apprecitated. Indeed, he didn't provide that "why" and tbf that wasn't the point of the article. But thanks for adding that context.
> You missed the whole "real world systems". E.g. like stock trading, where zero stock trades are tombstones.
Hm I don't think I missed that. This counts as "on the wire". Externally, there are surely good reasons for that representation, though I'd argue that internally it's better to represent this in the type system instead of special casing 0 everywhere which can be forgotten and then you get your (potential) division-by-0 issues. Avoiding them by construction is even better than failing explicitly (which I agree is in turn still better than silently returning 0).
I'm not sure what you mean exactly? There is no soundness issue here, the fact that `sqrt -1` is defined to be 0 does not have any impact on what statements about `sqrt x` can be proved when `x` is positive.
It just means that if you are working on an intermediate step of a proof and you need the result that `sqrt y >= 0` you don't need to provide a proof that `y >= 0`. If you wanted an intermediate result that `(sqrt y) * 2 = y` then you would still need to provide a proof that `y >= 0`, though.
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.
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.
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 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...
What is a coordinate in the context of a rational number? How many coordinates does it have?