Comment by hyperhello
12 hours ago
The point of writing Lean code is that Lean checks it accordingly. Lean is a domain specific language to encode mathematical reasoning in a way that can’t be fooled.
Note to other users: don’t downvote this kind of comment, answer it.
I would be a bit careful asserting that in full generality, given https://github.com/James-Hanson/junk-theorems-in-lean
This has nothing to do with Lean, e.g.
> The first coordinate of the polynomial X^2 (X^3 + X + 1 ) is equal to the prime factorization of 30 .
We defined polynomials as their coefficient functions in my algebra class, and it makes sense that you'd define a prime factorization as a function from primes to N, which naturally extends to a function N->N. So this junk theorem is part of normal math too. It just says in an obtuse way that they're both the function that's 1 at 2, 3, and 5, and 0 elsewhere.
junk theorems aren't the concern, soundness issues in the lean kernel are the concern.
Notably, junk theorems are true. Nobody would debate that the junk theorem is true. The main thing people would say is that junk theorems, while being true, are sensitive to precisely how you encoded mathematics, so despite being true, they are perhaps not conceptually meaningful.
As an example of a junk theorem, sasy you use the definition of the natural numbers using von neumann ordinals
https://en.wikipedia.org/wiki/Set-theoretic_definition_of_na...
Then for any natural numbers n, m, they're implicitly sets. So n \intersect m = min(n,m). This is the wrong way to think about natural numbers. You should not use this ever in proofs. But this isn't because your proofs would be false, but instead because it is a fundamentally confusing way to think about the natural numbers. It is in this sense it is a "junk theorem".
Isn’t there some theorem that any sufficiently complex mathematical languages will have statements that can’t be proven? :)
This would be funny if it were relevant. Seems like a statement about false negatives instead of false positives.
False negative = could not find a proof of a true theorem.
False positive = erroneous proof of a theorem.
Is Lean a DSL? I’d argue it’s a general purpose programming language that excels at proofs.
Well, there’s actually a very small set of operations that allow all computation, so it doesn’t take much to be a DSL and a GP too; I’d be surprised if a proof language couldn’t swing it.
it is a general-purpose programming language. for example, it's standard library allows you to do file io, networking, etc.