3 ms·

Well, I'm not a mathematician, but it seems like if it's really trivial, it shouldn't be hard to formalize on a high level why it's true, like almost in natural

Well, I'm not a mathematician, but it seems like if it's really trivial, it shouldn't be hard to formalize on a high level why it's true, like almost in natural language and then compile that high-level expression into a lower level argument. And if it's hard to even do that, then is the statement really trivial, or is it perhaps something that seems intuitive, but may not be sure (perhaps some pathological edge case may apply)?

gpm 7y ago
So here's a dumb example I just came up with. Let's say we know that x = 3^a 5^b. It's a trivial fact at this point that x isn't divisible by 2 (by the fact that prime factorization is unique). Disclaimer: I'm not actually good enough with lean to prove this sort of statement quickly... I could be under or even over selling lean here, hence why I phrased my original comment as a question about whether I was missing something. If I was trying to prove this formally, I'd have to say something like (in computer speak): Suppose x is divisible by 2, x = 2 * y, y has a prime factorization p by <theorem in library>, and 2 * p is therefore a prime factorization of x (ouch, already not sure how to specify that statement). 2 * p = x = 3^a 5^b, so 2 * p = 3^a 5^b. Both are prime factorizations, prime factorizations are unique by <theorem>, therefore both expressions should have the same number of 2 terms, but the one on the left has at least one, and the one on the right has 0, so they don't. This is a contradiction, so x is not divisible by two. You see why I'd like a computer to fill in the long formal proof instead of doing it myself? It's not because the statement might be false, it's because it's a pain to phrase everything in terms of the re-usable result about unique prime factorization. While I'm disclaiming things, disclaimer 2: I'm a hobbyist, not a real mathematician.
- bonoboTP 7y ago
  I didn't mean that the necessary high level tools exist today. It may very well be that computerized formal proof systems are at the stage where programming was when only assembly existed. It was very tedious to express what you wanted. I think the analogy is quite close:in both cases you're trying to express an idea very precisely, for an uncompromisingly literal-minded computer. I was formulating a vision with ergonomic tooling, helpful language constructs that haven't been invented yet, etc.
  - gpm 7y ago
    But that big paragraph is the natural language version of the formal proof. It's less strict and has more helpful concepts than any programming language in the world. It's that big because there actually are a lot of details needed for the proof. For instance it's not necessarily true that x = y = z means x = z, I need to provide a proof of that (transitivity of equality), it's not necessarily true that just because x = 3^a 5^b doesn't mean x isn't also 2 * <some other prime factorization>, I need a proof of that. Etc. Unless the computer is smart enough to do all that work for me. In which case the language isn't just nicer, it's also got an automated theorem prover. Something like lean isn't assembly, it's a full fledged language with abstractions, better IDE support than I've seen for any "real" programming language, the ability to program new "tactics" (methods of proof), and so on. I'm not trying to prove things in raw logic in it. The thing is I don't want to be trying to prove some of these things at all, I want the reader (the compiler) to just go ahead and supply their own proof.

gpm 7y ago

So here's a dumb example I just came up with. Let's say we know that x = 3^a 5^b. It's a trivial fact at this point that x isn't divisible by 2 (by the fact that prime factorization is unique). Disclaimer: I'm not actually good enough with lean to prove this sort of statement quickly... I could be under or even over selling lean here, hence why I phrased my original comment as a question about whether I was missing something. If I was trying to prove this formally, I'd have to say something like (in computer speak): Suppose x is divisible by 2, x = 2 * y, y has a prime factorization p by <theorem in library>, and 2 * p is therefore a prime factorization of x (ouch, already not sure how to specify that statement). 2 * p = x = 3^a 5^b, so 2 * p = 3^a 5^b. Both are prime factorizations, prime factorizations are unique by <theorem>, therefore both expressions should have the same number of 2 terms, but the one on the left has at least one, and the one on the right has 0, so they don't. This is a contradiction, so x is not divisible by two. You see why I'd like a computer to fill in the long formal proof instead of doing it myself? It's not because the statement might be false, it's because it's a pain to phrase everything in terms of the re-usable result about unique prime factorization. While I'm disclaiming things, disclaimer 2: I'm a hobbyist, not a real mathematician.

bonoboTP 7y ago
I didn't mean that the necessary high level tools exist today. It may very well be that computerized formal proof systems are at the stage where programming was when only assembly existed. It was very tedious to express what you wanted. I think the analogy is quite close:in both cases you're trying to express an idea very precisely, for an uncompromisingly literal-minded computer. I was formulating a vision with ergonomic tooling, helpful language constructs that haven't been invented yet, etc.
- gpm 7y ago
  But that big paragraph is the natural language version of the formal proof. It's less strict and has more helpful concepts than any programming language in the world. It's that big because there actually are a lot of details needed for the proof. For instance it's not necessarily true that x = y = z means x = z, I need to provide a proof of that (transitivity of equality), it's not necessarily true that just because x = 3^a 5^b doesn't mean x isn't also 2 * <some other prime factorization>, I need a proof of that. Etc. Unless the computer is smart enough to do all that work for me. In which case the language isn't just nicer, it's also got an automated theorem prover. Something like lean isn't assembly, it's a full fledged language with abstractions, better IDE support than I've seen for any "real" programming language, the ability to program new "tactics" (methods of proof), and so on. I'm not trying to prove things in raw logic in it. The thing is I don't want to be trying to prove some of these things at all, I want the reader (the compiler) to just go ahead and supply their own proof.